now

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

end;

hence Im f is with_the_same_dom Functional_Sequence of X,REAL by MESFUNC8:def 2; :: thesis: verum