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();
A2: for y being object st y in Y holds
ex z being object st S₂[y,z]

proof

let y be object ; :: thesis: ( y in Y implies ex z being object st S₂[y,z] )
assume y in Y ; :: thesis: ex z being object st S₂[y,z]
then reconsider y = y as Function by A1;
take y . x ; :: thesis: S₂[y,y . x]
take y ; :: thesis: ( y = y & y . x = y . x )
thus ( y = y & y . x = y . x ) ; :: thesis: verum

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);
take rng f ; :: thesis: for y being object holds
( y in rng f iff ex f being Function st
( f in X & y = f . x ) )
let y be object ; :: thesis: ( y in rng f iff ex f being Function st
( f in X & y = f . x ) )
thus ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) :: thesis: ( ex f being Function st
( f in X & y = f . x ) implies y in rng f )

proof

assume y in rng f ; :: thesis: ex f being Function st
( f in X & y = f . x )
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: ( g in X & y = g . x )
thus ( g in X & y = g . x ) by A1, A3, A4, A5, A6, A7; :: thesis: verum

end;

given g being Function such that A8: g in X and
A9: y = g . x ; :: thesis: y in rng f
A10: g in Y by A1, A8;
then ex f1 being Function st
( g = f1 & f . g = f1 . x ) by A3;
hence y in rng f by A3, A9, A10, FUNCT_1:def 3; :: thesis: verum