proposition: Lemma IntegralLstable : forall {IS : IntegrationSpace} (f : PartialFunction (X (ElemFunc IS))) (fL : L (ElemFunc IS) f), Integral (IntegrableL f fL) == I IS f fL.
proof: Proof. intros. unfold IntegrableL. pose proof (IntegralCv (IntegralRepresentationL f fL)). apply (CR_cv_unique (fun n => I IS f fL)). 2: apply CR_cv_const. apply (CR_cv_eq _ (CRsum (fun n : nat => I IS (IntFn (IntegralRepresentationL f fL) n) (IntFnL (IntegralRepresentationL f fL) n)))). 2: exact H. intro n. destruct n. reflexivity. symmetry. rewrite <- CRplus_0_r, decomp_sum. apply CRplus_morph. apply IExtensional. intros. apply DomainProp. rewrite (CRsum_eq _ (fun _ => 0)). rewrite sum_eq_R0. reflexivity. intros _. reflexivity. intros. simpl. apply Izero_is_zero. apply le_n_S, Nat.le_0_l. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase