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 );
A2: 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
A3: ( dom f = Y & ( for y being set st y in Y holds
S₂[y,f . y] ) ) from CLASSES1:sch 1(A2);

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
A4: z in dom f and
A5: y = f . z by FUNCT_1:def 5;
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 5; :: thesis: verum

end;

then rng f = pi X,x by Def6;
then A11: card (pi X,x) c= card Y by A3, 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 A11, XBOOLE_1:1; :: thesis: verum