let X be non empty set ; for f being PartFunc of X,COMPLEX
for c being Complex holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
let f be PartFunc of X,COMPLEX; for c being Complex holds
( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
let c be Complex; ( Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f)) & Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f)) )
A1:
dom ((Re c) (#) (Re f)) = dom (Re f)
by VALUED_1:def 5;
A2:
dom ((Im c) (#) (Im f)) = dom (Im f)
by VALUED_1:def 5;
A3:
dom (c (#) f) = dom f
by VALUED_1:def 5;
A4:
dom (Re (c (#) f)) = dom (c (#) f)
by COMSEQ_3:def 3;
A5:
dom (Re f) = dom f
by COMSEQ_3:def 3;
A6:
dom (Im f) = dom f
by COMSEQ_3:def 4;
A7:
dom (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) = (dom ((Re c) (#) (Re f))) /\ (dom ((Im c) (#) (Im f)))
by VALUED_1:12;
now for x being object st x in dom (Re (c (#) f)) holds
(Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . xlet x be
object ;
( x in dom (Re (c (#) f)) implies (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x )A8:
Re (c * (f . x)) = ((Re c) * (Re (f . x))) - ((Im c) * (Im (f . x)))
by COMPLEX1:9;
assume A9:
x in dom (Re (c (#) f))
;
(Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . xthen A10:
((Im c) (#) (Im f)) . x = (Im c) * ((Im f) . x)
by A4, A6, A2, A3, VALUED_1:def 5;
A11:
(Im f) . x = Im (f . x)
by A4, A6, A3, A9, COMSEQ_3:def 4;
A12:
(Re f) . x = Re (f . x)
by A4, A5, A3, A9, COMSEQ_3:def 3;
(Re (c (#) f)) . x = Re ((c (#) f) . x)
by A9, COMSEQ_3:def 3;
then A13:
(Re (c (#) f)) . x = Re (c * (f . x))
by A4, A9, VALUED_1:def 5;
((Re c) (#) (Re f)) . x = (Re c) * ((Re f) . x)
by A4, A5, A1, A3, A9, VALUED_1:def 5;
hence
(Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x
by A4, A5, A6, A1, A2, A3, A7, A9, A13, A10, A12, A11, A8, VALUED_1:13;
verum end;
hence
Re (c (#) f) = ((Re c) (#) (Re f)) - ((Im c) (#) (Im f))
by A4, A5, A6, A1, A2, A3, A7, FUNCT_1:2; Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f))
A14:
dom ((Im c) (#) (Re f)) = dom (Re f)
by VALUED_1:def 5;
A15:
dom ((Re c) (#) (Im f)) = dom (Im f)
by VALUED_1:def 5;
A16:
dom (Im (c (#) f)) = dom (c (#) f)
by COMSEQ_3:def 4;
A17:
dom (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) = (dom ((Im c) (#) (Re f))) /\ (dom ((Re c) (#) (Im f)))
by VALUED_1:def 1;
now for x being object st x in dom (Im (c (#) f)) holds
(Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . xlet x be
object ;
( x in dom (Im (c (#) f)) implies (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x )assume A18:
x in dom (Im (c (#) f))
;
(Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . xthen A19:
((Im c) (#) (Re f)) . x = (Im c) * ((Re f) . x)
by A5, A16, A14, A3, VALUED_1:def 5;
(Im (c (#) f)) . x = Im ((c (#) f) . x)
by A18, COMSEQ_3:def 4;
then A20:
(Im (c (#) f)) . x = Im (c * (f . x))
by A16, A18, VALUED_1:def 5;
A21:
(Im f) . x = Im (f . x)
by A16, A6, A3, A18, COMSEQ_3:def 4;
A22:
(Re f) . x = Re (f . x)
by A5, A16, A3, A18, COMSEQ_3:def 3;
A23:
((Re c) (#) (Im f)) . x = (Re c) * ((Im f) . x)
by A16, A6, A15, A3, A18, VALUED_1:def 5;
(((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x = (((Im c) (#) (Re f)) . x) + (((Re c) (#) (Im f)) . x)
by A5, A16, A6, A14, A15, A3, A17, A18, VALUED_1:def 1;
hence
(Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x
by A20, A19, A23, A22, A21, COMPLEX1:9;
verum end;
hence
Im (c (#) f) = ((Im c) (#) (Re f)) + ((Re c) (#) (Im f))
by A5, A16, A6, A14, A15, A3, A17, FUNCT_1:2; verum