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 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 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 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 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; :: 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:13;
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 :: thesis: for x being Element of X st x in dom (c (#) f) holds
(c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x

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:5;
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;
thus 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
.= c * (Integral (M,f)) by A1 ; :: thesis: verum