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

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

end;

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