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) ) )
assume A1: f is_integrable_on M ; :: thesis: ( r (#) f is_integrable_on M & Integral M,(r (#) f) = r * (Integral M,f) )
then A2: ( Re f is_integrable_on M & Im f is_integrable_on M ) by Def4;
then A3: ( r (#) (Re f) is_integrable_on M & Integral M,(r (#) (Re f)) = (R_EAL r) * (Integral M,(Re f)) & r (#) (Im f) is_integrable_on M & Integral M,(r (#) (Im f)) = (R_EAL r) * (Integral M,(Im f)) ) by MESFUNC6:102;
then A4: ( Re (r (#) f) is_integrable_on M & Im (r (#) f) is_integrable_on M & Integral M,(r (#) (Re f)) = Integral M,(Re (r (#) f)) & Integral M,(r (#) (Im f)) = Integral M,(Im (r (#) f)) ) by COM21r;
then A5: r (#) f is_integrable_on M by Def4;
( -infty < Integral M,(Re f) & Integral M,(Re f) < +infty & -infty < Integral M,(Im f) & Integral M,(Im f) < +infty ) by A2, MESFUNC6:90;
then reconsider R1 = Integral M,(Re f), I1 = Integral M,(Im f) as Real by XXREAL_0:14;
( -infty < Integral M,(Re (r (#) f)) & Integral M,(Re (r (#) f)) < +infty & -infty < Integral M,(Im (r (#) f)) & Integral M,(Im (r (#) f)) < +infty ) by A4, MESFUNC6:90;
then reconsider R2 = Integral M,(Re (r (#) f)), I2 = Integral M,(Im (r (#) f)) as Real by XXREAL_0:14;
( (R_EAL r) * (R_EAL R1) = r * R1 & (R_EAL r) * (R_EAL I1) = r * I1 ) by Th7a;
then R2 + (I2 * <i> ) = r * (R1 + (I1 * <i> )) by A3, A4;
then Integral M,(r (#) f) = r * (R1 + (I1 * <i> )) by A5, Def5;
hence ( r (#) f is_integrable_on M & Integral M,(r (#) f) = r * (Integral M,f) ) by A4, A1, Def5, Def4; :: thesis: verum