let x be object ; :: thesis:
let X be set ; :: thesis:
consider Y being set such that
A1: for y being object holds
( y in Y iff ( y in X & S₁[y] ) ) from XBOOLE_0:sch 1();
defpred S₂[ object , object ] means ex g being Function st
( $1 = g & $2 = g . x );
A2: for y being object st y in Y holds
ex z being object st S₂[y,z]

let y be object ; :: thesis:
assume y in Y ; :: thesis:
then reconsider y = y as Function by A1;
take y . x ; :: thesis:
take y ; :: thesis:
thus ( y = y & y . x = y . x ) ; :: thesis:

end;

consider f being Function such that
A3: ( dom f = Y & ( for y being object st y in Y holds
S₂[y,f . y] ) ) from CLASSES1:sch 1(A2);

let y be object ; :: thesis:
thus ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) :: thesis:

assume y in rng f ; :: thesis:
then consider z being object such that
A4: z in dom f and
A5: y = f . z by FUNCT_1:def 3;
consider g being Function such that
A6: z = g and
A7: f . z = g . x by A3, A4;
take g ; :: thesis:
thus ( g in X & y = g . x ) by A1, A3, A4, A5, A6, A7; :: thesis:

end;

end;