let x be object ; for X being set holds card (pi (X,x)) c= card X
let X be set ; 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 & S1[y] ) )
from XBOOLE_0:sch 1();
defpred S2[ 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 S2[y,z]
proof
let y be
object ;
( y in Y implies ex z being object st S2[y,z] )
assume
y in Y
;
ex z being object st S2[y,z]
then reconsider y =
y as
Function by A1;
take
y . x
;
S2[y,y . x]
take
y
;
( y = y & y . x = y . x )
thus
(
y = y &
y . x = y . x )
;
verum
end;
consider f being Function such that
A3:
( dom f = Y & ( for y being object st y in Y holds
S2[y,f . y] ) )
from CLASSES1:sch 1(A2);
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; verum