A1:
( dom (Re f) = dom f & dom (Im f) = dom f )
by COMSEQ_3:def 3, COMSEQ_3:def 4;
dom (Im f) = dom (<i> (#) (Im f))
by VALUED_1:def 5;
then A2: dom (Im f) =
(dom (Re f)) /\ (dom (<i> (#) (Im f)))
by A1
.=
dom ((Re f) + (<i> (#) (Im f)))
by VALUED_1:def 1
;
for k being object st k in dom ((Re f) + (<i> (#) (Im f))) holds
((Re f) + (<i> (#) (Im f))) . k = f . k
proof
let k be
object ;
( k in dom ((Re f) + (<i> (#) (Im f))) implies ((Re f) + (<i> (#) (Im f))) . k = f . k )
assume B1:
k in dom ((Re f) + (<i> (#) (Im f)))
;
((Re f) + (<i> (#) (Im f))) . k = f . k
B2:
Re (((Re f) + (<i> (#) (Im f))) . k) =
(Re ((Re f) + (<i> (#) (Im f)))) . k
by A1, A2, B1, COMSEQ_3:def 3
.=
Re (f . k)
by B1, A1, A2, COMSEQ_3:def 3
;
Im (((Re f) + (<i> (#) (Im f))) . k) =
(Im ((Re f) + (<i> (#) (Im f)))) . k
by A2, B1, COMSEQ_3:def 4
.=
Im (f . k)
by A2, B1, COMSEQ_3:def 4
;
hence
((Re f) + (<i> (#) (Im f))) . k = f . k
by B2, COMPLEX1:3;
verum
end;
hence
(Re f) + (<i> (#) (Im f)) = f
by A2, COMSEQ_3:def 4; verum