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;

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;

( 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

hence
Re (f + g) = (Re f) + (Re g)
by A4, FUNCT_1:2; :: thesis: Im (f + g) = (Im f) + (Im g)(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;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

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

hence
Im (f + g) = (Im f) + (Im g)
by A12, FUNCT_1:2; :: thesis: verum(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;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