for y being object st y in the carrier of (M ./. R) holds
y in rng (nat_hom R)

proof

let y be object ; :: thesis: ( y in the carrier of (M ./. R) implies y in rng (nat_hom R) )
assume y in the carrier of (M ./. R) ; :: thesis: y in rng (nat_hom R)
then consider x being object such that
A1: ( x in the carrier of M & y = Class (R,x) ) by EQREL_1:def 3;
reconsider x = x as Element of M by A1;
the carrier of M = dom (nat_hom R) by FUNCT_2:def 1;
then ( x in dom (nat_hom R) & (nat_hom R) . x = Class (R,x) ) by Def6;
hence y in rng (nat_hom R) by A1, FUNCT_1:def 3; :: thesis: verum

end;

then the carrier of (M ./. R) c= rng (nat_hom R) ;
then rng (nat_hom R) = the carrier of (M ./. R) by XBOOLE_0:def 10;
hence nat_hom R is onto by FUNCT_2:def 3; :: thesis: verum