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) ) )
A1: c = (Re c) + ((Im c) * <i> ) by COMPLEX1:29;
A2: dom (<i> (#) f) = dom f by VALUED_1:def 5;
assume A3: f is_integrable_on M ; :: thesis: ( c (#) f is_integrable_on M & Integral M,(c (#) f) = c * (Integral M,f) )
then A4: Integral M,((Re c) (#) f) = (Re c) * (Integral M,f) by Th38;
A5: <i> (#) f is_integrable_on M by A3, Th39;
then A6: (Im c) (#) (<i> (#) f) is_integrable_on M by Th38;
A7: (Re c) (#) f is_integrable_on M by A3, Th38;
then consider E being Element of S such that
A8: E = (dom ((Re c) (#) f)) /\ (dom ((Im c) (#) (<i> (#) f))) and
A9: Integral M,(((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) = (Integral M,(((Re c) (#) f) | E)) + (Integral M,(((Im c) (#) (<i> (#) f)) | E)) by A6, Th36;
A10: dom (c (#) f) = dom f by VALUED_1:def 5;
A11: Integral M,((Im c) (#) (<i> (#) f)) = (Im c) * (Integral M,(<i> (#) f)) by A5, Th38;
A12: dom ((Re c) (#) f) = dom f by VALUED_1:def 5;
A13: dom ((Im c) (#) (<i> (#) f)) = dom (<i> (#) f) by VALUED_1:def 5;
A14: 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 A15: x in dom (c (#) f) ; :: thesis: (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x
then A16: (c (#) f) . x = c * (f . x) by VALUED_1:def 5;
A17: ((Im c) (#) (<i> (#) f)) . x = (Im c) * ((<i> (#) f) . x) by A10, A2, A13, A15, VALUED_1:def 5;
A18: ((Re c) (#) f) . x = (Re c) * (f . x) by A10, A12, A15, VALUED_1:def 5;
A19: (<i> (#) f) . x = <i> * (f . x) by A10, A2, A15, VALUED_1:def 5;
(((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x = (((Re c) (#) f) . x) + (((Im c) (#) (<i> (#) f)) . x) by A10, A12, A2, A13, A14, A15, VALUED_1:def 1;
hence (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x by A1, A16, A18, A17, A19; :: thesis: verum

end;

then A20: c (#) f = ((Re c) (#) f) + ((Im c) (#) (<i> (#) f)) by A10, A12, A2, A13, A14, PARTFUN1:34;
hence c (#) f is_integrable_on M by A7, A6, Th33; :: thesis: Integral M,(c (#) f) = c * (Integral M,f)
A21: Integral M,(<i> (#) f) = <i> * (Integral M,f) by A3, Th39;
((Re c) (#) f) | E = (Re c) (#) f by A12, A2, A13, A8, RELAT_1:97;
hence Integral M,(c (#) f) = ((Re c) * (Integral M,f)) + (((Im c) * <i> ) * (Integral M,f)) by A12, A2, A13, A20, A4, A21, A11, A8, A9, RELAT_1:97
.= c * (Integral M,f) by A1 ;
:: thesis: verum