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 st f is_integrable_on M holds
( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX st f is_integrable_on M holds
( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )
let f be PartFunc of X,COMPLEX; :: thesis: ( f is_integrable_on M implies ( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) ) )
A1: Re (<i> (#) f) = - (Im f) by Th4;
assume A2: f is_integrable_on M ; :: thesis: ( <i> (#) f is_integrable_on M & Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) )
then A3: Im f is_integrable_on M by Def4;
A4: Im (<i> (#) f) = Re f by Th4;
then A5: Im (<i> (#) f) is_integrable_on M by A2, Def4;
- (Im f) = (- 1) (#) (Im f) ;
then Re (<i> (#) f) is_integrable_on M by A3, A1, MESFUNC6:102;
hence <i> (#) f is_integrable_on M by A5, Def4; :: thesis: Integral (M,(<i> (#) f)) = <i> * (Integral (M,f))
then consider R1, I1 being Real such that
A6: R1 = Integral (M,(Re (<i> (#) f))) and
A7: I1 = Integral (M,(Im (<i> (#) f))) and
A8: Integral (M,(<i> (#) f)) = R1 + (I1 * <i>) by Def5;
consider R, I being Real such that
A9: R = Integral (M,(Re f)) and
A10: I = Integral (M,(Im f)) and
A11: Integral (M,f) = R + (I * <i>) by A2, Def5;
R1 = (R_EAL (- 1)) * (R_EAL I) by A3, A1, A10, A6, MESFUNC6:102
.= (- 1) * I by EXTREAL1:5 ;
hence Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) by A4, A9, A11, A7, A8; :: thesis: verum