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 ; :: thesis: ( 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))) ; :: thesis: ((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; :: thesis: verum

end;

hence (Re f) + (<i> (#) (Im f)) = f by A2, COMSEQ_3:def 4; :: thesis: verum