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

proof

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

end;

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