proposition: Lemma IntegrationSpaceComplete : forall (IS : IntegrationSpace) (f : PartialFunction (X (ElemFunc IS))), @IntegrableFunction (IntegrationSpaceCompletion IS) f -> L (ElemFunc (IntegrationSpaceCompletion IS)) f.
proof: Proof. intros IS f fInt. simpl. destruct fInt, x. destruct (IntegrableFunctionsComplete IS IntFn IntFnL IntAbsSum IntAbsSumCv). exists x. destruct x. simpl. simpl in p0. apply (PartialRestriction_trans _ _ (XinfiniteSumAbs IntFn)). apply p0. exact p. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveCauchyAbs ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions CMTbase CMTIntegrableFunctions