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