let X be non empty set ; :: thesis: for P being a_partition of X
for c being Cardinal st ( for x being Element of X holds card (EqClass (x,P)) = c ) holds
card X = c *` (card P)
let P be a_partition of X; :: thesis: for c being Cardinal st ( for x being Element of X holds card (EqClass (x,P)) = c ) holds
card X = c *` (card P)
let c be Cardinal; :: thesis: ( ( for x being Element of X holds card (EqClass (x,P)) = c ) implies card X = c *` (card P) )
assume A1: for x being Element of X holds card (EqClass (x,P)) = c ; :: thesis: card X = c *` (card P)
for A, B being set st A in P & B in P & A <> B holds
A misses B by EQREL_1:def 4;
then A2: P is mutually-disjoint by TAXONOM2:def 5;

now :: thesis: for A being set st A in P holds
card A = c

let A be set ; :: thesis: ( A in P implies card A = c )
set a = the Element of A;
assume A3: A in P ; :: thesis: card A = c
then A4: A is Subset of X ;
A <> {} by A3, EQREL_1:def 4;
then A5: the Element of A in A ;
then reconsider a = the Element of A as Element of X by A4;
A = EqClass (a,P) by A3, A5, EQREL_1:def 6;
hence card A = c by A1; :: thesis: verum

end;

then card (union P) = c *` (card P) by A2, Th56;
hence card X = c *` (card P) by EQREL_1:def 4; :: thesis: verum