let X be set ; :: thesis: for P being a_partition of X holds card P c= card X
let P be a_partition of X; :: thesis: card P c= card X
defpred S₁[ set , set ] means $2 = choose $1;
P: for e being set st e in P holds
ex u being set st S₁[e,u] ;
consider f being Function such that
A: dom f = P and
B: for e being set st e in P holds
S₁[e,f . e] from CLASSES1:sch 1(P);
C: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A1: x1 in dom f and
B1: x2 in dom f and
C1: f . x1 = f . x2 ; :: thesis: x1 = x2
D1: x1 <> {} by A, A1, EQREL_1:def 6;
E1: x2 <> {} by A, B1, EQREL_1:def 6;
( f . x1 = choose x1 & f . x2 = choose x2 ) by A1, B1, A, B;
then x1 meets x2 by C1, D1, E1, XBOOLE_0:3;
hence x1 = x2 by A1, B1, A, EQREL_1:def 6; :: thesis: verum

end;

rng f c= X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in X )
assume y in rng f ; :: thesis: y in X
then consider x being set such that
A1: x in dom f and
B1: y = f . x by FUNCT_1:def 5;
C1: f . x = choose x by A, B, A1;
x <> {} by A, A1, EQREL_1:def 6;
then f . x in x by C1;
hence y in X by A1, A, B1; :: thesis: verum

end;

hence card P c= card X by A, C, CARD_1:26; :: thesis: verum