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

proof

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

end;

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