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;
A1: for e being set st e in P holds
ex u being set st S₁[e,u] ;
consider f being Function such that
A2: dom f = P and
A3: for e being set st e in P holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
A4: f is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A5: x1 in dom f and
A6: x2 in dom f and
A7: f . x1 = f . x2 ; :: thesis: x1 = x2
A8: x1 <> {} by A2, A5, EQREL_1:def 4;
A9: x2 <> {} by A2, A6, EQREL_1:def 4;
( f . x1 = choose x1 & f . x2 = choose x2 ) by A5, A6, A2, A3;
then x1 meets x2 by A7, A8, A9, XBOOLE_0:3;
hence x1 = x2 by A5, A6, A2, EQREL_1:def 4; :: 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
A10: x in dom f and
A11: y = f . x by FUNCT_1:def 3;
A12: f . x = choose x by A2, A3, A10;
x <> {} by A2, A10, EQREL_1:def 4;
then f . x in x by A12;
hence y in X by A10, A2, A11; :: thesis: verum

end;

hence card P c= card X by A2, A4, CARD_1:10; :: thesis: verum