proposition: Lemma IElemProductHomogeneous : forall { I J : IntegrationSpace } (a : CRcarrier (RealT (ElemFunc I))) (f : PartialFunction (prod (X (ElemFunc I)) (X (ElemFunc J)))) (fL : L (ProductFunctionRieszSpace I J) f), IElemProduct (Xscale a f) (LscaleStable (ProductFunctionRieszSpace I J) a f fL) == a * (IElemProduct f fL).
proof: Proof. intros. simpl; unfold IElemProduct; destruct fL as [l fL]. clear fL f. induction l. - simpl. rewrite CRmult_0_r. reflexivity. - simpl. rewrite IHl. do 2 rewrite CRmult_assoc. rewrite <- CRmult_plus_distr_l. apply CRmult_morph. reflexivity. rewrite CRmult_assoc. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile