let c be CR_coefficients of m; :: thesis: c is INT -valued

hence c is INT -valued by RELAT_1:def 19; :: thesis: verum

now :: thesis: for u being object st u in rng c holds

u in INT

then
rng c c= INT
by TARSKI:def 3;u in INT

let u be object ; :: thesis: ( u in rng c implies u in INT )

assume u in rng c ; :: thesis: u in INT

then consider x being object such that

A1: x in dom c and

A2: c . x = u by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A1;

reconsider x = x as Nat ;

ex s, mm being Integer st

( mm = (Product m) / (m . x) & s * mm,1 are_congruent_mod m . x & c . x = s * ((Product m) / (m . x)) ) by A1, Def4;

hence u in INT by A2, INT_1:def 2; :: thesis: verum

end;assume u in rng c ; :: thesis: u in INT

then consider x being object such that

A1: x in dom c and

A2: c . x = u by FUNCT_1:def 3;

reconsider x = x as Element of NAT by A1;

reconsider x = x as Nat ;

ex s, mm being Integer st

( mm = (Product m) / (m . x) & s * mm,1 are_congruent_mod m . x & c . x = s * ((Product m) / (m . x)) ) by A1, Def4;

hence u in INT by A2, INT_1:def 2; :: thesis: verum

hence c is INT -valued by RELAT_1:def 19; :: thesis: verum