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 (Im ((Re f) + (<i> (#) (Im f)))) holds
(Im ((Re f) + (<i> (#) (Im f)))) . k = (Im f) . k

proof

let k be object ; :: thesis: ( k in dom (Im ((Re f) + (<i> (#) (Im f)))) implies (Im ((Re f) + (<i> (#) (Im f)))) . k = (Im f) . k )
assume B1: k in dom (Im ((Re f) + (<i> (#) (Im f)))) ; :: thesis: (Im ((Re f) + (<i> (#) (Im f)))) . k = (Im f) . k
then B2: k in dom ((Re f) + (<i> (#) (Im f))) by COMSEQ_3:def 4;
then B3: k in (dom (Re f)) /\ (dom (<i> (#) (Im f))) by VALUED_1:def 1;
(Im ((Re f) + (<i> (#) (Im f)))) . k = Im (((Re f) + (<i> (#) (Im f))) . k) by B1, COMSEQ_3:def 4
.= Im (((Re f) . k) + ((<i> (#) (Im f)) . k)) by B2, VALUED_1:def 1
.= Im (((Re f) . k) + (<i> * ((Im f) . k))) by B3, VALUED_1:def 5
.= (Im ((Re f) . k)) + (Im (<i> * ((Im f) . k))) by COMPLEX1:8
.= 0 + ((Im f) . k) ;
hence (Im ((Re f) + (<i> (#) (Im f)))) . k = (Im f) . k ; :: thesis: verum

end;

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