let c be CR_coefficients of m; :: thesis: c is integer-yielding

now

let u be set ; :: thesis: ( u in rng c implies u in INT )
assume u in rng c ; :: thesis: u in INT
then consider x being set 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 natural number ;
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 integer-yielding by VALUED_0:def 5; :: thesis: verum