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

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