now

let y be set ; :: 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 set such that
A1: x in dom (mod u,m) and
A2: (mod u,m) . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A1;
reconsider x = x as natural number ;
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 integer-yielding by VALUED_0:def 5; :: thesis: verum