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) ) )

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) )
reconsider E = {} as finite set ;
take E ; :: thesis: ( E = union X & card E = k * (card X) )
thus ( E = union X & card E = k * (card X) ) by A1, CARD_1:47, 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: S₁[ {}. D] by ZFMISC_1:2;
A3: 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
A4: ( ( 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
A5: not s in S and
A6: 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.})) )

now

let Y be set ; :: thesis: ( Y in S implies Y is finite )
assume A7: Y in S ; :: thesis: Y is finite
s in {s} by TARSKI:def 1;
then ( Y in S \/ {s} & s in S \/ {s} & s <> Y ) by A5, A7, 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 A6;
hence Y is finite ; :: thesis: verum

end;

then reconsider D1 = union S as finite set by FINSET_1:25;
A8: union {s} = s by ZFMISC_1:31;
s in {s} by TARSKI:def 1;
then s in S \/ {s} by XBOOLE_0:def 3;
then consider B being finite set such that
A9: ( 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 A6;
reconsider T = s as finite set by A9;

A10: now

assume union S meets union {s} ; :: thesis: contradiction
then consider x being set such that
A11: ( x in union S & x in union {s} ) by XBOOLE_0:3;
consider Y being set such that
A12: x in Y and
A13: Y in S by A11, TARSKI:def 4;
consider Z being set such that
A14: x in Z and
A15: Z in {s} by A11, TARSKI:def 4;
A16: ( Z <> Y & Z in S \/ {s} & Y in S \/ {s} ) by A5, A13, A15, TARSKI:def 1, XBOOLE_0:def 3;
then consider B being finite set such that
A17: ( 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 A6;
Y misses Z by A16, A17;
hence contradiction by A12, A14, XBOOLE_0:3; :: thesis: verum

end;

A18: union (S \/ {s}) = D1 \/ T by A8, ZFMISC_1:96;
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.}))

A19: now

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
A20: ( 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 A6;
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 A20; :: 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
A21: Z in S and
A22: Y <> Z ; :: thesis: ( Y,Z are_equipotent & Y misses Z )
Z in S \/ {s} by A21, XBOOLE_0:def 3;
hence ( Y,Z are_equipotent & Y misses Z ) by A20, A22; :: thesis: verum

end;

A23: card (S \/ {s}) = (card S) + 1 by A5, CARD_2:54;
thus card D2 = (k * (card S)) + (k * 1) by A4, A8, A9, A10, A18, A19, CARD_2:53
.= k * (card (S \/ {s})) by A23 ; :: thesis: verum

end;

A24: for B being Element of Fin D holds S₁[B] from SETWISEO:sch 2(A2, A3);
X is Element of Fin D by FINSUB_1:def 5;
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 A24; :: thesis: verum

end;

end;