now :: thesis: for y being object st y in rng (mod (u,m)) holds
y in INT

let y be object ; :: thesis: ( y in rng (mod (u,m)) implies y in INT )
assume y in rng (mod (u,m)) ; :: thesis: y in INT
then consider x being object such that
A1: x in dom (mod (u,m)) and
A2: (mod (u,m)) . x = y by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1;
reconsider x = x as Nat ;
y = u mod (m . x) by A1, A2, Def3;
hence y in INT by INT_1:def 2; :: thesis: verum

end;

then rng (mod (u,m)) c= INT by TARSKI:def 3;
hence mod (u,m) is INT -valued by RELAT_1:def 19; :: thesis: verum