defpred S₁[ object , object ] means ex v being Element of M st
( $1 = v & $2 = Class (R,v) );
A1: for x being object st x in the carrier of M holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in the carrier of M implies ex y being object st S₁[x,y] )
assume x in the carrier of M ; :: thesis: ex y being object st S₁[x,y]
then reconsider v = x as Element of M ;
reconsider y = Class (R,v) as set ;
take y ; :: thesis: S₁[x,y]
take v ; :: thesis: ( x = v & y = Class (R,v) )
thus ( x = v & y = Class (R,v) ) ; :: thesis: verum

end;

consider f being Function such that
A2: dom f = the carrier of M and
A3: for x being object st x in the carrier of M holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
rng f c= the carrier of (M ./. R)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in the carrier of (M ./. R) )
assume x in rng f ; :: thesis: x in the carrier of (M ./. R)
then consider y being object such that
A4: y in dom f and
A5: f . y = x by FUNCT_1:def 3;
consider v being Element of M such that
A6: ( y = v & f . y = Class (R,v) ) by A2, A3, A4;
thus x in the carrier of (M ./. R) by A5, A6, EQREL_1:def 3; :: thesis: verum

end;

then reconsider f = f as Function of M,(M ./. R) by A2, FUNCT_2:def 1, RELSET_1:4;
take f ; :: thesis: for v being Element of M holds f . v = Class (R,v)
let v be Element of M; :: thesis: f . v = Class (R,v)
ex w being Element of M st
( v = w & f . v = Class (R,w) ) by A3;
hence f . v = Class (R,v) ; :: thesis: verum