let x be object ; :: thesis: for X being set holds card (pi (X,x)) c= card X
let X be set ; :: thesis: card (pi (X,x)) c= card X
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]

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);

now :: thesis: for y being object holds
( ( 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 ) )

let y be object ; :: 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 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

end;

then rng f = pi (X,x) by Def6;
then A11: card (pi (X,x)) c= card Y by A3, CARD_1:12;
Y c= X by A1;
then card Y c= card X by CARD_1:11;
hence card (pi (X,x)) c= card X by A11; :: thesis: verum