( dom (Re f) = dom f & dom (Im f) = dom f ) by COMSEQ_3:def 3, COMSEQ_3:def 4;
then dom (Re f) = dom (<i> (#) (Im f)) by VALUED_1:def 5;
then A2: dom (Re f) = (dom (Re f)) /\ (dom (<i> (#) (Im f)))
.= dom ((Re f) + (<i> (#) (Im f))) by VALUED_1:def 1 ;
for k being object st k in dom (Re ((Re f) + (<i> (#) (Im f)))) holds
(Re ((Re f) + (<i> (#) (Im f)))) . k = (Re f) . k

proof

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

end;

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