let X be non empty set ; :: thesis: for f, g being PartFunc of X,COMPLEX holds
( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
let f, g be PartFunc of X,COMPLEX; :: thesis: ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
A1: dom ((Re f) (#) (Re g)) = (dom (Re f)) /\ (dom (Re g)) by VALUED_1:def 4;
A2: dom ((Im f) (#) (Im g)) = (dom (Im f)) /\ (dom (Im g)) by VALUED_1:def 4;
A3: dom (Re f) = dom f by COMSEQ_3:def 3;
A4: dom (Im g) = dom g by COMSEQ_3:def 4;
A5: dom (Re g) = dom g by COMSEQ_3:def 3;
A6: dom (Re (f (#) g)) = dom (f (#) g) by COMSEQ_3:def 3;
then A7: dom (Re (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def 4;
A8: dom (Im f) = dom f by COMSEQ_3:def 4;
A9: dom (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) = (dom ((Re f) (#) (Re g))) /\ (dom ((Im f) (#) (Im g))) by VALUED_1:12;

now :: thesis: for x being object st x in dom (Re (f (#) g)) holds
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x

let x be object ; :: thesis: ( x in dom (Re (f (#) g)) implies (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x )
assume A10: x in dom (Re (f (#) g)) ; :: thesis: (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x
then (Re (f (#) g)) . x = Re ((f (#) g) . x) by COMSEQ_3:def 3;
then (Re (f (#) g)) . x = Re ((f . x) * (g . x)) by A6, A10, VALUED_1:def 4;
then A11: (Re (f (#) g)) . x = ((Re (f . x)) * (Re (g . x))) - ((Im (f . x)) * (Im (g . x))) by COMPLEX1:9;
x in dom g by A7, A10, XBOOLE_0:def 4;
then A12: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def 3, COMSEQ_3:def 4;
x in dom f by A7, A10, XBOOLE_0:def 4;
then ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def 3, COMSEQ_3:def 4;
then (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) . x) * ((Im g) . x)) by A7, A1, A3, A5, A10, A11, A12, VALUED_1:def 4;
then (Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) (#) (Im g)) . x) by A7, A2, A8, A4, A10, VALUED_1:def 4;
hence (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x by A7, A9, A1, A2, A3, A8, A5, A4, A10, VALUED_1:13; :: thesis: verum

end;

hence Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) by A7, A9, A1, A2, A3, A8, A5, A4, FUNCT_1:2; :: thesis: Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
A13: dom ((Im f) (#) (Re g)) = (dom (Im f)) /\ (dom (Re g)) by VALUED_1:def 4;
A14: dom ((Re f) (#) (Im g)) = (dom (Re f)) /\ (dom (Im g)) by VALUED_1:def 4;
A15: dom (Im (f (#) g)) = dom (f (#) g) by COMSEQ_3:def 4;
then A16: dom (Im (f (#) g)) = (dom f) /\ (dom g) by VALUED_1:def 4;
A17: dom (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) = (dom ((Im f) (#) (Re g))) /\ (dom ((Re f) (#) (Im g))) by VALUED_1:def 1;

now :: thesis: for x being object st x in dom (Im (f (#) g)) holds
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x

let x be object ; :: thesis: ( x in dom (Im (f (#) g)) implies (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x )
assume A18: x in dom (Im (f (#) g)) ; :: thesis: (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x
then (Im (f (#) g)) . x = Im ((f (#) g) . x) by COMSEQ_3:def 4;
then (Im (f (#) g)) . x = Im ((f . x) * (g . x)) by A15, A18, VALUED_1:def 4;
then A19: (Im (f (#) g)) . x = ((Im (f . x)) * (Re (g . x))) + ((Re (f . x)) * (Im (g . x))) by COMPLEX1:9;
x in dom g by A16, A18, XBOOLE_0:def 4;
then A20: ( (Re g) . x = Re (g . x) & (Im g) . x = Im (g . x) ) by A5, A4, COMSEQ_3:def 3, COMSEQ_3:def 4;
x in dom f by A16, A18, XBOOLE_0:def 4;
then ( (Re f) . x = Re (f . x) & (Im f) . x = Im (f . x) ) by A3, A8, COMSEQ_3:def 3, COMSEQ_3:def 4;
then (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) . x) * ((Im g) . x)) by A16, A13, A8, A5, A18, A19, A20, VALUED_1:def 4;
then (Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) (#) (Im g)) . x) by A16, A14, A3, A4, A18, VALUED_1:def 4;
hence (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x by A16, A17, A13, A14, A3, A8, A5, A4, A18, VALUED_1:def 1; :: thesis: verum

end;

hence Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) by A16, A17, A13, A14, A3, A8, A5, A4, FUNCT_1:2; :: thesis: verum