proposition: Lemma CSUCIntegralHomogeneous : forall {R : ConstructiveReals} (a : CRcarrier R) (f : PartialFunction (CRcarrier R)) (fL : Is_CSUC_func f), IntegralCSUC (Xscale a f) (CSUC_func_scale a f fL) == a * IntegralCSUC f fL.
proof: Proof. intros. unfold IntegralCSUC. rewrite <- UC_integral_scale. destruct f,fL; apply UC_integral_extens; reflexivity. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets