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 by Def4;
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, Def4;
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 Real by A5, A9, A10, XXREAL_0:14;
A11: (R_EAL r) * (R_EAL R1) = r * R1 by Th1;
A12: (R_EAL r) * (R_EAL I1) = r * I1 by Th1;
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 Real by A7, A14, A15, XXREAL_0:14;
A16: Integral M,(r (#) (Im f)) = (R_EAL r) * (Integral M,(Im f)) by A8, MESFUNC6:102;
A17: r (#) f is_integrable_on M by A6, A13, Def4;
Integral M,(r (#) (Re f)) = (R_EAL 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, Def5;
hence ( r (#) f is_integrable_on M & Integral M,(r (#) f) = r * (Integral M,f) ) by A3, A6, A13, Def4, Def5; :: thesis: verum