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
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,COMPLEX
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,COMPLEX
for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) )
let f be PartFunc of X,COMPLEX ; :: thesis: for c being complex number st f is_integrable_on M holds
( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) )
let c be complex number ; :: thesis: ( f is_integrable_on M implies ( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) ) )
assume A1: f is_integrable_on M ; :: thesis: ( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) )
A2: c = (Re c) + ((Im c) * <i> ) by COMPLEX1:29;
B1: ( dom (c (#) f) = dom f & dom ((Re c) (#) f) = dom f & dom (<i> (#) f) = dom f & dom ((Im c) (#) (<i> (#) f)) = dom (<i> (#) f) ) by VALUED_1:def 5;
B2: dom (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) (<i> (#) f))) by VALUED_1:def 1;

now

let x be Element of X; :: thesis: ( x in dom (c (#) f) implies (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x )
assume x in dom (c (#) f) ; :: thesis: (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x
then ( (c (#) f) . x = c * (f . x) & (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x = (((Re c) (#) f) . x) + (((Im c) (#) (<i> (#) f)) . x) & ((Re c) (#) f) . x = (Re c) * (f . x) & ((Im c) (#) (<i> (#) f)) . x = (Im c) * ((<i> (#) f) . x) & (<i> (#) f) . x = <i> * (f . x) ) by B1, B2, VALUED_1:def 1, VALUED_1:def 5;
hence (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x by A2; :: thesis: verum

end;

then A3: c (#) f = ((Re c) (#) f) + ((Im c) (#) (<i> (#) f)) by B1, B2, PARTFUN1:34;
A4: ( (Re c) (#) f is_integrable_on M & Integral M,((Re c) (#) f) = (Re c) * (Integral M,f) ) by A1, Th102r;
A5: ( <i> (#) f is_integrable_on M & Integral M,(<i> (#) f) = <i> * (Integral M,f) ) by A1, Th102c;
then A6: ( (Im c) (#) (<i> (#) f) is_integrable_on M & Integral M,((Im c) (#) (<i> (#) f)) = (Im c) * (Integral M,(<i> (#) f)) ) by Th102r;
hence c (#) f is_integrable_on M by A3, Th100, A4; :: thesis: Integral M,(c (#) f) = c * (Integral M,f)
consider E being Element of S such that
A7: ( E = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) (<i> (#) f))) & Integral M,(((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) = (Integral M,(((Re c) (#) f) | E)) + (Integral M,(((Im c) (#) (<i> (#) f)) | E)) ) by Th101, A4, A6;
((Re c) (#) f) | E = (Re c) (#) f by B1, A7, RELAT_1:97;
hence Integral M,(c (#) f) = ((Re c) * (Integral M,f)) + (((Im c) * <i> ) * (Integral M,f)) by A4, A6, A5, A3, A7, B1, RELAT_1:97
.= c * (Integral M,f) by A2 ;
:: thesis: verum