now :: thesis: for k, l being Nat holds dom ((Re f) . k) = dom ((Re f) . l)

let k, l be Nat; :: thesis: dom ((Re f) . k) = dom ((Re f) . l)
dom ((Re f) . k) = dom (f . k) by Def11;
then dom ((Re f) . k) = dom (f . l) by MESFUNC8:def 2;
hence dom ((Re f) . k) = dom ((Re f) . l) by Def11; :: thesis: verum

end;

hence Re f is with_the_same_dom by MESFUNC8:def 2; :: thesis: verum