let X be non empty set ; 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; 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; 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; 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; ( 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
; ( 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 for x being Element of X st x in dom (c (#) f) holds
(c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . xlet x be
Element of
X;
( x in dom (c (#) f) implies (c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . x )assume A15:
x in dom (c (#) f)
;
(c (#) f) . x = (((Re c) (#) f) + ((Im c) (#) (<i> (#) f))) . xthen 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;
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; 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
; verum