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 ;
A4: Im (<i> (#) f) = Re f by Th4;
then A5: Im (<i> (#) f) is_integrable_on M by A2;
Re (<i> (#) f) is_integrable_on M by A3, A1, MESFUNC6:102;
hence <i> (#) f is_integrable_on M by A5; :: 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 Def3;
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, Def3;
R1 = (- 1) * I by A3, A1, A10, A6, MESFUNC6:102
.= (- 1) * I ;
hence Integral (M,(<i> (#) f)) = <i> * (Integral (M,f)) by A4, A9, A11, A7, A8; :: thesis: verum