for k being object st k in dom (Re (Im f)) holds
(Re (Im f)) . k = (Im f) . k

proof

let k be object ; :: thesis: ( k in dom (Re (Im f)) implies (Re (Im f)) . k = (Im f) . k )
assume k in dom (Re (Im f)) ; :: thesis: (Re (Im f)) . k = (Im f) . k
then (Re (Im f)) . k = Re ((Im f) . k) by COMSEQ_3:def 3
.= (Im f) . k ;
hence (Re (Im f)) . k = (Im f) . k ; :: thesis: verum

end;

hence Re (Im f) = Im f by COMSEQ_3:def 3; :: thesis: verum