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,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let f be PartFunc of X,COMPLEX; :: thesis: for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let r be Real; :: thesis: ( f is_integrable_on M implies ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) )

A1: Integral (M,(r (#) (Re f))) = Integral (M,(Re (r (#) f))) by Th2;

A2: Integral (M,(r (#) (Im f))) = Integral (M,(Im (r (#) f))) by Th2;

assume A3: f is_integrable_on M ; :: thesis: ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

then A4: Re f is_integrable_on M ;

then A5: Integral (M,(Re f)) < +infty by MESFUNC6:90;

r (#) (Re f) is_integrable_on M by A4, MESFUNC6:102;

then A6: Re (r (#) f) is_integrable_on M by Th2;

then A7: Integral (M,(Re (r (#) f))) < +infty by MESFUNC6:90;

A8: Im f is_integrable_on M by A3;

then A9: -infty < Integral (M,(Im f)) by MESFUNC6:90;

A10: Integral (M,(Im f)) < +infty by A8, MESFUNC6:90;

-infty < Integral (M,(Re f)) by A4, MESFUNC6:90;

then reconsider R1 = Integral (M,(Re f)), I1 = Integral (M,(Im f)) as Element of REAL by A5, A9, A10, XXREAL_0:14;

A11: r * R1 = r * R1 ;

A12: r * I1 = r * I1 ;

r (#) (Im f) is_integrable_on M by A8, MESFUNC6:102;

then A13: Im (r (#) f) is_integrable_on M by Th2;

then A14: -infty < Integral (M,(Im (r (#) f))) by MESFUNC6:90;

A15: Integral (M,(Im (r (#) f))) < +infty by A13, MESFUNC6:90;

-infty < Integral (M,(Re (r (#) f))) by A6, MESFUNC6:90;

then reconsider R2 = Integral (M,(Re (r (#) f))), I2 = Integral (M,(Im (r (#) f))) as Element of REAL by A7, A14, A15, XXREAL_0:14;

A16: Integral (M,(r (#) (Im f))) = r * (Integral (M,(Im f))) by A8, MESFUNC6:102;

A17: r (#) f is_integrable_on M by A6, A13;

Integral (M,(r (#) (Re f))) = r * (Integral (M,(Re f))) by A4, MESFUNC6:102;

then R2 + (I2 * <i>) = r * (R1 + (I1 * <i>)) by A16, A1, A2, A11, A12;

then Integral (M,(r (#) f)) = r * (R1 + (I1 * <i>)) by A17, Def3;

hence ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) by A3, A6, A13, Def3; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX

for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let f be PartFunc of X,COMPLEX; :: thesis: for r being Real st f is_integrable_on M holds

( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

let r be Real; :: thesis: ( f is_integrable_on M implies ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) )

A1: Integral (M,(r (#) (Re f))) = Integral (M,(Re (r (#) f))) by Th2;

A2: Integral (M,(r (#) (Im f))) = Integral (M,(Im (r (#) f))) by Th2;

assume A3: f is_integrable_on M ; :: thesis: ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) )

then A4: Re f is_integrable_on M ;

then A5: Integral (M,(Re f)) < +infty by MESFUNC6:90;

r (#) (Re f) is_integrable_on M by A4, MESFUNC6:102;

then A6: Re (r (#) f) is_integrable_on M by Th2;

then A7: Integral (M,(Re (r (#) f))) < +infty by MESFUNC6:90;

A8: Im f is_integrable_on M by A3;

then A9: -infty < Integral (M,(Im f)) by MESFUNC6:90;

A10: Integral (M,(Im f)) < +infty by A8, MESFUNC6:90;

-infty < Integral (M,(Re f)) by A4, MESFUNC6:90;

then reconsider R1 = Integral (M,(Re f)), I1 = Integral (M,(Im f)) as Element of REAL by A5, A9, A10, XXREAL_0:14;

A11: r * R1 = r * R1 ;

A12: r * I1 = r * I1 ;

r (#) (Im f) is_integrable_on M by A8, MESFUNC6:102;

then A13: Im (r (#) f) is_integrable_on M by Th2;

then A14: -infty < Integral (M,(Im (r (#) f))) by MESFUNC6:90;

A15: Integral (M,(Im (r (#) f))) < +infty by A13, MESFUNC6:90;

-infty < Integral (M,(Re (r (#) f))) by A6, MESFUNC6:90;

then reconsider R2 = Integral (M,(Re (r (#) f))), I2 = Integral (M,(Im (r (#) f))) as Element of REAL by A7, A14, A15, XXREAL_0:14;

A16: Integral (M,(r (#) (Im f))) = r * (Integral (M,(Im f))) by A8, MESFUNC6:102;

A17: r (#) f is_integrable_on M by A6, A13;

Integral (M,(r (#) (Re f))) = r * (Integral (M,(Re f))) by A4, MESFUNC6:102;

then R2 + (I2 * <i>) = r * (R1 + (I1 * <i>)) by A16, A1, A2, A11, A12;

then Integral (M,(r (#) f)) = r * (R1 + (I1 * <i>)) by A17, Def3;

hence ( r (#) f is_integrable_on M & Integral (M,(r (#) f)) = r * (Integral (M,f)) ) by A3, A6, A13, Def3; :: thesis: verum