let k be Nat; :: thesis: for X being finite set st ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) holds
ex C being finite set st
( C = union X & card C = k * (card X) )
let X be finite set ; :: thesis: ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) )

per cases ( X = {} or X <> {} ) ;

suppose A1: X = {} ; :: thesis: ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) )

reconsider E = {} as finite set ;
assume for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ; :: thesis: ex C being finite set st
( C = union X & card C = k * (card X) )
take E ; :: thesis: ( E = union X & card E = k * (card X) )
thus ( E = union X & card E = k * (card X) ) by A1, CARD_1:27, ZFMISC_1:2; :: thesis: verum

end;

suppose X <> {} ; :: thesis: ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) )

then reconsider D = X as non empty set ;
defpred S₁[ Element of Fin D] means ( ( for Y being set st Y in $1 holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in $1 & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union $1 & card C = k * (card $1) ) );
A2: for S being Element of Fin D
for s being Element of D st S₁[S] & not s in S holds
S₁[S \/ {.s.}]

proof

let S be Element of Fin D; :: thesis: for s being Element of D st S₁[S] & not s in S holds
S₁[S \/ {.s.}]
let s be Element of D; :: thesis: ( S₁[S] & not s in S implies S₁[S \/ {.s.}] )
assume that
A3: ( ( for Y being set st Y in S holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union S & card C = k * (card S) ) ) and
A4: not s in S and
A5: for Y being set st Y in S \/ {s} holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ; :: thesis: ex C being finite set st
( C = union (S \/ {.s.}) & card C = k * (card (S \/ {.s.})) )
A6: card (S \/ {s}) = (card S) + 1 by A4, CARD_2:41;

now :: thesis: for Y being set st Y in S holds
Y is finite

let Y be set ; :: thesis: ( Y in S implies Y is finite )
assume Y in S ; :: thesis: Y is finite
then Y in S \/ {s} by XBOOLE_0:def 3;
then ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) by A5;
hence Y is finite ; :: thesis: verum

end;

then reconsider D1 = union S as finite set by FINSET_1:7;

A7: now :: thesis: for Y, Z being set st Y in S holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )

let Y, Z be set ; :: thesis: ( Y in S implies ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) )
assume Y in S ; :: thesis: ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )
then Y in S \/ {s} by XBOOLE_0:def 3;
then consider B being finite set such that
A8: ( B = Y & card B = k ) and
A9: for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) by A5;
take B = B; :: thesis: ( B = Y & card B = k & ( for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) )
thus ( B = Y & card B = k ) by A8; :: thesis: for Z being set st Z in S & Y <> Z holds
( Y,Z are_equipotent & Y misses Z )
let Z be set ; :: thesis: ( Z in S & Y <> Z implies ( Y,Z are_equipotent & Y misses Z ) )
assume that
A10: Z in S and
A11: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )
Z in S \/ {s} by A10, XBOOLE_0:def 3;
hence ( Y,Z are_equipotent & Y misses Z ) by A9, A11; :: thesis: verum

end;

s in {s} by TARSKI:def 1;
then s in S \/ {s} by XBOOLE_0:def 3;
then A12: ex B being finite set st
( B = s & card B = k & ( for Z being set st Z in S \/ {s} & s <> Z holds
( s,Z are_equipotent & s misses Z ) ) ) by A5;
then reconsider T = s as finite set ;
A13: union {s} = s by ZFMISC_1:25;
then A14: union (S \/ {s}) = D1 \/ T by ZFMISC_1:78;
then reconsider D2 = union (S \/ {s}) as finite set ;
take D2 ; :: thesis: ( D2 = union (S \/ {.s.}) & card D2 = k * (card (S \/ {.s.})) )
thus D2 = union (S \/ {s}) ; :: thesis: card D2 = k * (card (S \/ {.s.}))

now :: thesis: not union S meets union {s}

assume union S meets union {s} ; :: thesis: contradiction
then consider x being object such that
A15: x in union S and
A16: x in union {s} by XBOOLE_0:3;
consider Y being set such that
A17: x in Y and
A18: Y in S by A15, TARSKI:def 4;
consider Z being set such that
A19: x in Z and
A20: Z in {s} by A16, TARSKI:def 4;
A21: Z in S \/ {s} by A20, XBOOLE_0:def 3;
Y in S \/ {s} by A18, XBOOLE_0:def 3;
then A22: ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in S \/ {s} & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) by A5;
Z <> Y by A4, A18, A20, TARSKI:def 1;
then Y misses Z by A21, A22;
hence contradiction by A17, A19, XBOOLE_0:3; :: thesis: verum

end;

hence card D2 = (k * (card S)) + (k * 1) by A3, A13, A12, A14, A7, CARD_2:40
.= k * (card (S \/ {s})) by A6 ;
:: thesis: verum

end;

A23: X is Element of Fin D by FINSUB_1:def 5;
A24: S₁[ {}. D] by ZFMISC_1:2;
for B being Element of Fin D holds S₁[B] from SETWISEO:sch 2(A24, A2);
hence ( ( for Y being set st Y in X holds
ex B being finite set st
( B = Y & card B = k & ( for Z being set st Z in X & Y <> Z holds
( Y,Z are_equipotent & Y misses Z ) ) ) ) implies ex C being finite set st
( C = union X & card C = k * (card X) ) ) by A23; :: thesis: verum

end;

end;