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
H: ( x in dom c & c . x = u ) by FUNCT_1:def 5;
reconsider x = x as Element of NAT by H;
reconsider x = x as natural number ;
consider s, mm being Integer such that
Q: ( mm = (Product m) / (m . x) & s * mm,1 are_congruent_mod m . x & c . x = s * ((Product m) / (m . x)) ) by defCi, H;
thus u in INT by H, Q, 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