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) ) )
assume A1: f is_integrable_on M ; :: thesis: ( <i> (#) f is_integrable_on M & Integral M,(<i> (#) f) = <i> * (Integral M,f) )
then A2: ( Re f is_integrable_on M & Im f is_integrable_on M ) by Def4;
A3: ( Re (<i> (#) f) = - (Im f) & Im (<i> (#) f) = Re f ) by COM21c;
- (Im f) = (- 1) (#) (Im f) ;
then ( Re (<i> (#) f) is_integrable_on M & Im (<i> (#) f) is_integrable_on M ) by A2, A3, MESFUNC6:102;
hence A5: <i> (#) f is_integrable_on M by Def4; :: thesis: Integral M,(<i> (#) f) = <i> * (Integral M,f)
consider R, I being Real such that
A6: ( R = Integral M,(Re f) & I = Integral M,(Im f) & Integral M,f = R + (I * <i> ) ) by A1, Def5;
consider R1, I1 being Real such that
A7: ( R1 = Integral M,(Re (<i> (#) f)) & I1 = Integral M,(Im (<i> (#) f)) & Integral M,(<i> (#) f) = R1 + (I1 * <i> ) ) by A5, Def5;
R1 = (R_EAL (- 1)) * (R_EAL I) by A3, A7, A6, A2, MESFUNC6:102
.= (- 1) * I by EXTREAL1:38 ;
hence Integral M,(<i> (#) f) = <i> * (Integral M,f) by A3, A6, A7; :: thesis: verum