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:38 ;
hence Integral M,(<i> (#) f) = <i> * (Integral M,f) by A4, A9, A11, A7, A8; :: thesis: verum