proposition: Lemma IElemProductOneL : forall { I J : IntegrationSpace } (A : X (ElemFunc I) -> Prop) (B : X (ElemFunc J) -> Prop) (Aint : IntegrableSet A) (Bint : IntegrableSet B) (alpha : CRcarrier (RealT (ElemFunc I))), L (ProductFunctionRieszSpace I J) (ProdIntegrableFunc (Build_ProdIntegrable I J A B alpha Aint Bint)).
proof: Proof. intros. exists ((Build_ProdIntegrable I J A B alpha Aint Bint) :: nil). split. - intros [x y] H; apply H. - intros. simpl in xD, xG. unfold ProdLFunc. rewrite <- (CRplus_0_r ( partialApply (ProdIntegrableFunc {| prodint_f := A; prodint_g := B; prodint_factor := alpha; prodint_fint := Aint; prodint_gint := Bint |}) x xG)). destruct xD. apply CRplus_morph. apply DomainProp. reflexivity. Defined.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile