let c be CR_coefficients of m; :: thesis: c is INT -valued
now :: thesis: for u being object st u in rng c holds
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;
then rng c c= INT by TARSKI:def 3;
hence c is INT -valued by RELAT_1:def 19; :: thesis: verum