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 + g) = (Im f) + (Im g) )
let f, g be PartFunc of X,COMPLEX; :: thesis: ( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )
A1: dom (Re (f + g)) = dom (f + g) by COMSEQ_3:def 3;
A2: dom (Re g) = dom g by COMSEQ_3:def 3;
A3: dom (Re f) = dom f by COMSEQ_3:def 3;
then dom ((Re f) + (Re g)) = (dom f) /\ (dom g) by A2, VALUED_1:def 1;
then A4: dom (Re (f + g)) = dom ((Re f) + (Re g)) by A1, VALUED_1:def 1;

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

let x be object ; :: thesis: ( x in dom (Re (f + g)) implies (Re (f + g)) . x = ((Re f) + (Re g)) . x )
assume A5: x in dom (Re (f + g)) ; :: thesis: (Re (f + g)) . x = ((Re f) + (Re 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 A1, A5, VALUED_1:def 1;
then A6: (Re (f + g)) . x = (Re (f . x)) + (Re (g . x)) by COMPLEX1:8;
A7: x in (dom f) /\ (dom g) by A1, A5, VALUED_1:def 1;
then x in dom (Re g) by A2, XBOOLE_0:def 4;
then A8: (Re g) . x = Re (g . x) by COMSEQ_3:def 3;
x in dom (Re f) by A3, A7, XBOOLE_0:def 4;
then (Re f) . x = Re (f . x) by COMSEQ_3:def 3;
hence (Re (f + g)) . x = ((Re f) + (Re g)) . x by A4, A5, A6, A8, VALUED_1:def 1; :: thesis: verum

end;

hence Re (f + g) = (Re f) + (Re g) by A4, FUNCT_1:2; :: thesis: Im (f + g) = (Im f) + (Im g)
A9: dom (Im (f + g)) = dom (f + g) by COMSEQ_3:def 4;
A10: dom (Im g) = dom g by COMSEQ_3:def 4;
A11: dom (Im f) = dom f by COMSEQ_3:def 4;
then dom ((Im f) + (Im g)) = (dom f) /\ (dom g) by A10, VALUED_1:def 1;
then A12: dom (Im (f + g)) = dom ((Im f) + (Im g)) by A9, VALUED_1:def 1;

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

let x be object ; :: thesis: ( x in dom (Im (f + g)) implies (Im (f + g)) . x = ((Im f) + (Im g)) . x )
assume A13: x in dom (Im (f + g)) ; :: thesis: (Im (f + g)) . x = ((Im 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 A9, A13, VALUED_1:def 1;
then A14: (Im (f + g)) . x = (Im (f . x)) + (Im (g . x)) by COMPLEX1:8;
A15: x in (dom f) /\ (dom g) by A9, A13, VALUED_1:def 1;
then x in dom (Im g) by A10, XBOOLE_0:def 4;
then A16: (Im g) . x = Im (g . x) by COMSEQ_3:def 4;
x in dom (Im f) by A11, A15, XBOOLE_0:def 4;
then (Im f) . x = Im (f . x) by COMSEQ_3:def 4;
hence (Im (f + g)) . x = ((Im f) + (Im g)) . x by A12, A13, A14, A16, VALUED_1:def 1; :: thesis: verum

end;

hence Im (f + g) = (Im f) + (Im g) by A12, FUNCT_1:2; :: thesis: verum