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) )
A0: ( dom (Re (f + g)) = dom (f + g) & dom (Re f) = dom f & dom (Re g) = dom g ) by Def1;
then dom ((Re f) + (Re g)) = (dom f) /\ (dom g) by VALUED_1:def 1;
then C1: dom (Re (f + g)) = dom ((Re f) + (Re g)) by A0, VALUED_1:def 1;

now

let x be set ; :: thesis: ( x in dom (Re (f + g)) implies (Re (f + g)) . x = ((Re f) + (Re g)) . x )
assume P01: x in dom (Re (f + g)) ; :: thesis: (Re (f + g)) . x = ((Re f) + (Re g)) . x
then P03: x in (dom f) /\ (dom g) by A0, VALUED_1:def 1;
(Re (f + g)) . x = Re ((f + g) . x) by P01, Def1;
then (Re (f + g)) . x = Re ((f . x) + (g . x)) by A0, P01, VALUED_1:def 1;
then Q02: (Re (f + g)) . x = (Re (f . x)) + (Re (g . x)) by COMPLEX1:19;
( x in dom (Re f) & x in dom (Re g) ) by A0, P03, XBOOLE_0:def 4;
then ( (Re f) . x = Re (f . x) & (Re g) . x = Re (g . x) ) by Def1;
hence (Re (f + g)) . x = ((Re f) + (Re g)) . x by Q02, P01, C1, VALUED_1:def 1; :: thesis: verum

end;

hence Re (f + g) = (Re f) + (Re g) by C1, FUNCT_1:9; :: thesis: Im (f + g) = (Im f) + (Im g)
B0: ( dom (Im (f + g)) = dom (f + g) & dom (Im f) = dom f & dom (Im g) = dom g ) by Def2;
then dom ((Im f) + (Im g)) = (dom f) /\ (dom g) by VALUED_1:def 1;
then C2: dom (Im (f + g)) = dom ((Im f) + (Im g)) by B0, VALUED_1:def 1;

now

let x be set ; :: thesis: ( x in dom (Im (f + g)) implies (Im (f + g)) . x = ((Im f) + (Im g)) . x )
assume P01: x in dom (Im (f + g)) ; :: thesis: (Im (f + g)) . x = ((Im f) + (Im g)) . x
then P03: x in (dom f) /\ (dom g) by B0, VALUED_1:def 1;
(Im (f + g)) . x = Im ((f + g) . x) by P01, Def2;
then (Im (f + g)) . x = Im ((f . x) + (g . x)) by B0, P01, VALUED_1:def 1;
then Q02: (Im (f + g)) . x = (Im (f . x)) + (Im (g . x)) by COMPLEX1:19;
( x in dom (Im f) & x in dom (Im g) ) by B0, P03, XBOOLE_0:def 4;
then ( (Im f) . x = Im (f . x) & (Im g) . x = Im (g . x) ) by Def2;
hence (Im (f + g)) . x = ((Im f) + (Im g)) . x by Q02, P01, C2, VALUED_1:def 1; :: thesis: verum

end;

hence Im (f + g) = (Im f) + (Im g) by C2, FUNCT_1:9; :: thesis: verum