Example of a Complete Metric Space: IntegrableFunction

Definition IntegrableFunction := Complete L1StepQ.

Definition ∫ : IntegrableFunction --> CR :=
 Cmap L1StepQPrelengthSpace IntegralQ_uc.

Every bounded function is integrable.
Definition BoundedAsIntegrable : BoundedFunction --> IntegrableFunction :=
 Cmap LinfStepQPrelengthSpace LinfAsL1.