let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for c being Real st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for c being Real st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )
let f be PartFunc of X,ExtREAL ; :: thesis: for c being Real st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )
let c be Real; :: thesis: ( f is_integrable_on M implies ( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) ) )
assume A1: f is_integrable_on M ; :: thesis: ( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )
consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) by A1, Def17;
A3: ( c (#) f is_measurable_on A & dom (c (#) f) = A ) by A2, Th55, MESFUNC1:def 6;
A4: ( 0 <= integral+ M,(max+ f) & integral+ M,(max+ f) <> +infty & 0 <= integral+ M,(max- f) & integral+ M,(max- f) <> +infty ) by A1, Def17, Th102;
then reconsider I1 = integral+ M,(max+ f) as Real by XXREAL_0:14;
reconsider I2 = integral+ M,(max- f) as Real by A4, XXREAL_0:14;
A5: ( max+ f is nonnegative & max- f is nonnegative ) by Lm1;
A6: ( dom (max+ f) = A & dom (max- f) = A ) by A2, MESFUNC2:def 2, MESFUNC2:def 3;
A7: ( max+ f is_measurable_on A & max- f is_measurable_on A ) by A2, MESFUNC2:27, MESFUNC2:28;

per cases ( 0 <= c or c < 0 ) ;

suppose A8: 0 <= c ; :: thesis: ( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )

then A9: ( max+ (c (#) f) = c (#) (max+ f) & max- (c (#) f) = c (#) (max- f) ) by Th32;
A10: ( integral+ M,(c (#) (max+ f)) = (R_EAL c) * (integral+ M,(max+ f)) & integral+ M,(c (#) (max- f)) = (R_EAL c) * (integral+ M,(max- f)) ) by A5, A6, A7, A8, Th92;
( c * I1 is Real & c * I2 is Real ) ;
then ( (R_EAL c) * (integral+ M,(max+ f)) is Real & (R_EAL c) * (integral+ M,(max- f)) is Real ) by EXTREAL1:13;
then ( integral+ M,(max+ (c (#) f)) < +infty & (R_EAL c) * (integral+ M,(max- f)) < +infty ) by A9, A10, XXREAL_0:9;
hence c (#) f is_integrable_on M by A3, A9, A10, Def17; :: thesis: Integral M,(c (#) f) = (R_EAL c) * (Integral M,f)
thus Integral M,(c (#) f) = (integral+ M,(c (#) (max+ f))) - (integral+ M,(max- (c (#) f))) by A8, Th32
.= (integral+ M,(c (#) (max+ f))) - (integral+ M,(c (#) (max- f))) by A8, Th32
.= ((R_EAL c) * (integral+ M,(max+ f))) - (integral+ M,(c (#) (max- f))) by A5, A6, A7, A8, Th92
.= ((R_EAL c) * (integral+ M,(max+ f))) - ((R_EAL c) * (integral+ M,(max- f))) by A5, A6, A7, A8, Th92
.= (R_EAL c) * (Integral M,f) by XXREAL_3:112 ; :: thesis: verum

end;

suppose S: c < 0 ; :: thesis: ( c (#) f is_integrable_on M & Integral M,(c (#) f) = (R_EAL c) * (Integral M,f) )

- (- c) = c ;
then consider a being Real such that
A12: ( c = - a & a > 0 ) by S;
A13: ( max+ (c (#) f) = a (#) (max- f) & max- (c (#) f) = a (#) (max+ f) ) by A12, Th33;
A14: ( integral+ M,(a (#) (max- f)) = (R_EAL a) * (integral+ M,(max- f)) & integral+ M,(a (#) (max+ f)) = (R_EAL a) * (integral+ M,(max+ f)) ) by A5, A6, A7, A12, Th92;
( a * I2 is Real & a * I1 is Real ) ;
then ( (R_EAL a) * (integral+ M,(max- f)) is Real & (R_EAL a) * (integral+ M,(max+ f)) is Real ) by EXTREAL1:13;
then ( integral+ M,(max+ (c (#) f)) < +infty & (R_EAL a) * (integral+ M,(max+ f)) < +infty ) by A13, A14, XXREAL_0:9;
hence c (#) f is_integrable_on M by A3, A13, A14, Def17; :: thesis: Integral M,(c (#) f) = (R_EAL c) * (Integral M,f)
A15: - (R_EAL a) = - a by SUPINF_2:3;
thus Integral M,(c (#) f) = ((R_EAL a) * (integral+ M,(max- f))) - (integral+ M,(a (#) (max+ f))) by A5, A6, A7, A12, A13, Th92
.= ((R_EAL a) * (integral+ M,(max- f))) - ((R_EAL a) * (integral+ M,(max+ f))) by A5, A6, A7, A12, Th92
.= (R_EAL a) * ((integral+ M,(max- f)) - (integral+ M,(max+ f))) by XXREAL_3:112
.= (R_EAL a) * (- ((integral+ M,(max+ f)) - (integral+ M,(max- f)))) by XXREAL_3:27
.= - ((R_EAL a) * ((integral+ M,(max+ f)) - (integral+ M,(max- f)))) by XXREAL_3:103
.= (R_EAL c) * (Integral M,f) by A12, A15, XXREAL_3:103 ; :: thesis: verum

end;

end;