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

proof

let y be set ; :: thesis: ( y in Y implies ex z being set st S₂[y,z] )
assume y in Y ; :: thesis: ex z being set 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
A4: ( dom f = Y & ( for y being set st y in Y holds
S₂[y,f . y] ) ) from CLASSES1:sch 1(A3);

now

let y be set ; :: thesis: ( ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) & ( ex g being Function st
( g in X & y = g . x ) implies y in rng f ) )
thus ( y in rng f implies ex f being Function st
( f in X & y = f . x ) ) :: thesis: ( ex g being Function st
( g in X & y = g . 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 set such that
A5: ( z in dom f & y = f . z ) by FUNCT_1:def 5;
consider g being Function such that
A6: ( z = g & f . z = g . x ) by A4, A5;
take g ; :: thesis: ( g in X & y = g . x )
thus ( g in X & y = g . x ) by A1, A4, A5, A6; :: thesis: verum

end;

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

end;

then rng f = pi X,x by Def6;
then A9: card (pi X,x) c= card Y by A4, CARD_1:28;
Y c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in X )
thus ( not x in Y or x in X ) by A1; :: thesis: verum

end;

then card Y c= card X by CARD_1:27;
hence card (pi X,x) c= card X by A9, XBOOLE_1:1; :: thesis: verum