let P be set ; :: thesis: for c being Cardinal st P is mutually-disjoint & ( for A being set st A in P holds
card A = c ) holds
card (union P) = c *` (card P)
let c be Cardinal; :: thesis: ( P is mutually-disjoint & ( for A being set st A in P holds
card A = c ) implies card (union P) = c *` (card P) )
assume A1: ( P is mutually-disjoint & ( for A being set st A in P holds
card A = c ) ) ; :: thesis: card (union P) = c *` (card P)

per cases ( ( P <> {} & c <> 0 ) or ( P <> {} & c = 0 ) or P = {} ) ;

suppose A2: ( P <> {} & c <> 0 ) ; :: thesis: card (union P) = c *` (card P)

now :: thesis: union P <> {}

set A0 = the Element of P;
set a0 = the Element of the Element of P;
A3: the Element of P in P by A2;
card the Element of P <> 0 by A1, A2;
then the Element of P <> {} ;
then the Element of the Element of P in union P by A3, TARSKI:def 4;
hence union P <> {} ; :: thesis: verum

end;

then reconsider X = union P as non empty set ;

now :: thesis: for x being object st x in P holds
x in bool X

let x be object ; :: thesis: ( x in P implies x in bool X )
reconsider x0 = x as set by TARSKI:1;
assume x in P ; :: thesis: x in bool X
then x0 c= union P by SETFAM_1:41;
hence x in bool X ; :: thesis: verum

end;

then reconsider p = P as Subset-Family of X by TARSKI:def 3;

now :: thesis: for A being Subset of X st A in p holds
( A <> {} & ( for B being Subset of X st B in p & A <> B holds
A misses B ) )

let A be Subset of X; :: thesis: ( A in p implies ( A <> {} & ( for B being Subset of X st B in p & A <> B holds
A misses B ) ) )
assume A4: A in p ; :: thesis: ( A <> {} & ( for B being Subset of X st B in p & A <> B holds
A misses B ) )
then card A = c by A1;
hence A <> {} by A2; :: thesis: for B being Subset of X st B in p & A <> B holds
A misses B
let B be Subset of X; :: thesis: ( B in p & A <> B implies A misses B )
assume A5: B in p ; :: thesis: ( A <> B implies A misses B )
assume A <> B ; :: thesis: A misses B
hence A misses B by A1, A4, A5, TAXONOM2:def 5; :: thesis: verum

end;

then reconsider p = p as a_partition of X by EQREL_1:def 4;
deffunc H₁( set ) -> Enumeration of $1 = the Enumeration of $1;
deffunc H₂( object ) -> Element of bool X = EqClass ((In ($1,X)),p);
deffunc H₃( object ) -> object = [(H₁(H₂($1)) . $1),H₂($1)];
consider f being Function such that
A6: ( dom f = X & ( for x being object st x in X holds
f . x = H₃(x) ) ) from FUNCT_1:sch 3();

now :: thesis: for y being object holds
( ( y in [:c,P:] implies ex x being object st
( x in dom f & f . x = y ) ) & ( ex x being object st
( x in dom f & f . x = y ) implies y in [:c,P:] ) )

let y be object ; :: thesis: ( ( y in [:c,P:] implies ex x being object st
( x in dom f & f . x = y ) ) & ( ex x being object st
( x in dom f & f . x = y ) implies y in [:c,P:] ) )

hereby :: thesis: ( ex x being object st
( x in dom f & f . x = y ) implies y in [:c,P:] )

assume y in [:c,P:] ; :: thesis: ex x being object st
( x in dom f & f . x = y )
then consider d, A being object such that
A7: ( d in c & A in P & y = [d,A] ) by ZFMISC_1:def 2;
reconsider A = A as set by A7;
reconsider x = (H₁(A) ") . d as object ;
take x = x; :: thesis: ( x in dom f & f . x = y )
card A <> {} by A1, A7;
then A8: A = dom H₁(A) by FUNCT_2:def 1
.= rng (H₁(A) ") by FUNCT_1:33 ;
A9: c = card A by A1, A7
.= rng H₁(A) by FUNCT_2:def 3 ;
then c = dom (H₁(A) ") by FUNCT_1:33;
then A10: x in A by A7, A8, FUNCT_1:3;
hence A11: x in dom f by A6, A7; :: thesis: f . x = y
A c= X by A7, SETFAM_1:41;
then ( In (x,X) = x & A is Subset of X ) by A6, A11, SUBSET_1:def 8;
then A12: H₂(x) = A by A7, A10, EQREL_1:def 6;
thus f . x = [(H₁(A) . x),A] by A6, A11, A12
.= y by A7, A9, FUNCT_1:35 ; :: thesis: verum

end;

given x being object such that A13: ( x in dom f & f . x = y ) ; :: thesis: y in [:c,P:]
In (x,X) = x by A6, A13, SUBSET_1:def 8;
then A14: ( x in H₂(x) & H₂(x) in p ) by EQREL_1:def 6;
then x in dom H₁(H₂(x)) by FUNCT_2:def 1;
then H₁(H₂(x)) . x in rng H₁(H₂(x)) by FUNCT_1:3;
then H₁(H₂(x)) . x in card H₂(x) ;
then A15: H₁(H₂(x)) . x in c by A1, A14;
y = [(H₁(H₂(x)) . x),H₂(x)] by A6, A13;
hence y in [:c,P:] by A14, A15, ZFMISC_1:def 2; :: thesis: verum

end;

then A16: rng f = [:c,P:] by FUNCT_1:def 3;

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A17: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
then A18: ( f . x1 = [(H₁(H₂(x1)) . x1),H₂(x1)] & f . x2 = [(H₁(H₂(x2)) . x2),H₂(x2)] ) by A6;
then A19: H₂(x1) = H₂(x2) by A17, XTUPLE_0:1;
( In (x1,X) = x1 & In (x2,X) = x2 ) by A6, A17, SUBSET_1:def 8;
then A20: ( x1 in H₂(x1) & H₂(x1) in p & x2 in H₂(x1) ) by A19, EQREL_1:def 6;
then A21: dom H₁(H₂(x1)) = H₂(x1) by FUNCT_2:def 1;
H₁(H₂(x1)) . x1 = H₁(H₂(x1)) . x2 by A17, A18, A19, XTUPLE_0:1;
hence x1 = x2 by A20, A21, FUNCT_1:def 4; :: thesis: verum

end;

hence card (union P) = card (rng f) by A6, FUNCT_1:def 4, CARD_1:70
.= card [:c,(card P):] by A16, CARD_2:7
.= c *` (card P) by CARD_2:def 2 ;
:: thesis: verum

end;

suppose A22: ( P <> {} & c = 0 ) ; :: thesis: card (union P) = c *` (card P)

now :: thesis: for x, y being object st x in P & y in P holds
x = y

let x, y be object ; :: thesis: ( x in P & y in P implies x = y )
reconsider X = x, Y = y as set by TARSKI:1;
assume ( x in P & y in P ) ; :: thesis: x = y
then ( card X = 0 & card Y = 0 ) by A1, A22;
then ( X = {} & Y = {} ) ;
hence x = y ; :: thesis: verum

end;

then consider x being object such that
A23: P = {x} by A22, ZFMISC_1:def 10, ZFMISC_1:131;
reconsider X = x as set by TARSKI:1;
X in P by A23, TARSKI:def 1;
then card X = 0 by A1, A22;
then X = {} ;
then union P = {} by A23, ZFMISC_1:25;
hence card (union P) = c *` (card P) by A22, CARD_2:20; :: thesis: verum

end;

suppose P = {} ; :: thesis: card (union P) = c *` (card P)

hence card (union P) = c *` (card P) by CARD_2:20, ZFMISC_1:2; :: thesis: verum

end;

end;