let X be non empty set ; 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; 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; 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; 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; ( 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
; ( 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; verum