let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 :: thesis: for x being object st x in dom (Re (c (#) f)) holds
(Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x

let x be object ; :: thesis: ( 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)) ; :: thesis: (Re (c (#) f)) . x = (((Re c) (#) (Re f)) - ((Im c) (#) (Im f))) . x
then 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; :: thesis: 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; :: thesis: 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 :: thesis: for x being object st x in dom (Im (c (#) f)) holds
(Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x

let x be object ; :: thesis: ( 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)) ; :: thesis: (Im (c (#) f)) . x = (((Im c) (#) (Re f)) + ((Re c) (#) (Im f))) . x
then 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; :: thesis: 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; :: thesis: verum