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

y in INT

then
rng (mod (u,m)) c= INT
by TARSKI:def 3;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;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

hence mod (u,m) is INT -valued by RELAT_1:def 19; :: thesis: verum