:: CARD_2 semantic presentation

begin


theorem :: CARD_2:1
for x, X, Y being set st x in X & X,Y are_equipotent holds
( Y <> {} & ex x being set st x in Y )
proof
let x, X, Y be set ; ::_thesis: ( x in X & X,Y are_equipotent implies ( Y <> {} & ex x being set st x in Y ) )
assume A1: x in X ; ::_thesis: ( not X,Y are_equipotent or ( Y <> {} & ex x being set st x in Y ) )
given f being Function such that  f is one-to-one and
A2: ( dom f = X & rng f = Y ) ; :: according to WELLORD2:def_4 ::_thesis: ( Y <> {} & ex x being set st x in Y )
 f . x in Y by A1, A2, FUNCT_1:def_3;
hence  Y <> {} ; ::_thesis: ex x being set st x in Y
take  f . x ; ::_thesis: f . x in Y
thus  f . x in Y by A1, A2, FUNCT_1:def_3; ::_thesis: verum
end;

theorem :: CARD_2:2
for X being set holds
( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )
proof
let X be set ; ::_thesis: ( bool X, bool (card X) are_equipotent & card (bool X) = card (bool (card X)) )
consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by CARD_1:def_2, WELLORD2:def_4;
deffunc H1( set ) ->  set = f .: $1;
consider g being Function such that
A4: ( dom g = bool X & ( for x being set st x in bool X holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
thus  bool X, bool (card X) are_equipotent ::_thesis: card (bool X) = card (bool (card X))
proof
take  g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & proj1 g = bool X & proj2 g = bool (card X) )
thus  g is one-to-one ::_thesis: ( proj1 g = bool X & proj2 g = bool (card X) )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 g or not b1 in proj1 g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A5: x in dom g and
A6: y in dom g and
A7: g . x = g . y ; ::_thesis: x = y
A8: ( g . x = f .: x & g . y = f .: y ) by A4, A5, A6;
A9: y c= x
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in y or z in x )
assume A10: z in y ; ::_thesis: z in x
then  f . z in f .: y by A2, A4, A6, FUNCT_1:def_6;
then  ex u being set st
( u in dom f & u in x & f . z = f . u ) by A7, A8, FUNCT_1:def_6;
hence  z in x by A1, A2, A4, A6, A10, FUNCT_1:def_4; ::_thesis: verum
end;
 x c= y
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x or z in y )
assume A11: z in x ; ::_thesis: z in y
then  f . z in f .: x by A2, A4, A5, FUNCT_1:def_6;
then  ex u being set st
( u in dom f & u in y & f . z = f . u ) by A7, A8, FUNCT_1:def_6;
hence  z in y by A1, A2, A4, A5, A11, FUNCT_1:def_4; ::_thesis: verum
end;
hence  x = y by A9, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  dom g = bool X by A4; ::_thesis: proj2 g = bool (card X)
thus  rng g c= bool (card X) :: according to XBOOLE_0:def_10 ::_thesis: bool (card X) c= proj2 g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in bool (card X) )
assume  x in rng g ; ::_thesis: x in bool (card X)
then consider y being set  such that
A12: y in dom g and
A13: x = g . y by FUNCT_1:def_3;
A14: f .: y c= rng f by RELAT_1:111;
 g . y = f .: y by A4, A12;
hence  x in bool (card X) by A3, A13, A14; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in bool (card X) or x in proj2 g )
A15: f " x c= dom f by RELAT_1:132;
assume  x in bool (card X) ; ::_thesis: x in proj2 g
then  f .: (f " x) = x by A3, FUNCT_1:77;
then  g . (f " x) = x by A2, A4, A15;
hence  x in proj2 g by A2, A4, A15, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card (bool X) = card (bool (card X)) by CARD_1:5; ::_thesis: verum
end;

deffunc H1( set ) ->  set = $1 `1 ;

theorem :: CARD_2:3
for Z, X, Y being set st Z in Funcs (X,Y) holds
( Z,X are_equipotent & card Z = card X )
proof
let Z, X, Y be set ; ::_thesis: ( Z in Funcs (X,Y) implies ( Z,X are_equipotent & card Z = card X ) )
assume  Z in Funcs (X,Y) ; ::_thesis: ( Z,X are_equipotent & card Z = card X )
then consider f being Function such that
A1: Z = f and
A2: dom f = X and
 rng f c= Y by FUNCT_2:def_2;
thus  Z,X are_equipotent ::_thesis: card Z = card X
proof
consider g being Function such that
A3: ( dom g = Z & ( for x being set st x in Z holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
take  g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & proj1 g = Z & proj2 g = X )
thus  g is one-to-one ::_thesis: ( proj1 g = Z & proj2 g = X )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 g or not b1 in proj1 g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume that
A4: x in dom g and
A5: y in dom g ; ::_thesis: ( not g . x = g . y or x = y )
A6: ( g . x = x `1 & g . y = y `1 ) by A3, A4, A5;
 ex x1, x2 being set st [x1,x2] = y by A1, A3, A5, RELAT_1:def_1;
then A7: y = [(y `1),(y `2)] by MCART_1:8;
 ex x1, x2 being set st [x1,x2] = x by A1, A3, A4, RELAT_1:def_1;
then A8: x = [(x `1),(x `2)] by MCART_1:8;
then  x `2 = f . (x `1) by A1, A3, A4, FUNCT_1:1;
hence  ( not g . x = g . y or x = y ) by A1, A3, A5, A8, A7, A6, FUNCT_1:1; ::_thesis: verum
end;
thus  dom g = Z by A3; ::_thesis: proj2 g = X
thus  rng g c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= proj2 g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in X )
assume  x in rng g ; ::_thesis: x in X
then consider y being set  such that
A9: y in dom g and
A10: x = g . y by FUNCT_1:def_3;
 ex x1, x2 being set st [x1,x2] = y by A1, A3, A9, RELAT_1:def_1;
then A11: y = [(y `1),(y `2)] by MCART_1:8;
 x = y `1 by A3, A9, A10;
hence  x in X by A1, A2, A3, A9, A11, FUNCT_1:1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in proj2 g )
assume  x in X ; ::_thesis: x in proj2 g
then A12: [x,(f . x)] in Z by A1, A2, FUNCT_1:def_2;
then g . [x,(f . x)] = [x,(f . x)] `1 by A3
.= x ;
hence  x in proj2 g by A3, A12, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card Z = card X by CARD_1:5; ::_thesis: verum
end;

Lm1:  for A, B being Ordinal
for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
proof
let A, B be Ordinal; ::_thesis: for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
let x1, x2 be set ; ::_thesis: ( x1 <> x2 implies ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) )
defpred S1[ set ] means $1 in A;
deffunc H2( set ) ->  set = [$1,x1];
deffunc H3( Ordinal) ->  set = [($1 -^ A),x2];
consider f being Function such that
A1: dom f = A +^ B and
A2: for x being Ordinal st x in A +^ B holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H3(x) ) ) from FINSET_1:sch_1();
assume A3: x1 <> x2 ; ::_thesis: ( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) )
thus  A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent ::_thesis: card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:])
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = A +^ B & proj2 f = [:A,{x1}:] \/ [:B,{x2}:] )
thus  f is one-to-one ::_thesis: ( proj1 f = A +^ B & proj2 f = [:A,{x1}:] \/ [:B,{x2}:] )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A4: ( x in dom f & y in dom f ) and
A5: f . x = f . y ; ::_thesis: x = y
reconsider C1 = x, C2 = y as Ordinal by A1, A4;
percases ( ( x in A & y in A ) or ( not x in A & not y in A ) or ( x in A & not y in A ) or ( not x in A & y in A ) ) ;
supposeA6: ( x in A & y in A ) ; ::_thesis: x = y
A7: [x,x1] `1 = C1 ;
 ( f . C1 = [x,x1] & f . C2 = [y,x1] ) by A1, A2, A4, A6;
hence  x = y by A5, A7, MCART_1:7; ::_thesis: verum
end;
supposeA8: ( not x in A & not y in A ) ; ::_thesis: x = y
A9: [(C1 -^ A),x2] `1 = C1 -^ A ;
 ( f . x = [(C1 -^ A),x2] & f . y = [(C2 -^ A),x2] ) by A1, A2, A4, A8;
then A10: C1 -^ A = C2 -^ A by A5, A9, MCART_1:7;
 A c= C1 by A8, ORDINAL1:16;
then A11: C1 = A +^ (C1 -^ A) by ORDINAL3:def_5;
 A c= C2 by A8, ORDINAL1:16;
hence  x = y by A10, A11, ORDINAL3:def_5; ::_thesis: verum
end;
supposeA12: ( x in A & not y in A ) ; ::_thesis: x = y
A13: [x,x1] `2 = x1 ;
 ( f . x = [x,x1] & f . y = [(C2 -^ A),x2] ) by A1, A2, A4, A12;
hence  x = y by A3, A5, A13, MCART_1:7; ::_thesis: verum
end;
supposeA14: ( not x in A & y in A ) ; ::_thesis: x = y
A15: [y,x1] `2 = x1 ;
 ( f . y = [y,x1] & f . x = [(C1 -^ A),x2] ) by A1, A2, A4, A14;
hence  x = y by A3, A5, A15, MCART_1:7; ::_thesis: verum
end;
end;
end;
thus  dom f = A +^ B by A1; ::_thesis: proj2 f = [:A,{x1}:] \/ [:B,{x2}:]
thus  rng f c= [:A,{x1}:] \/ [:B,{x2}:] :: according to XBOOLE_0:def_10 ::_thesis: [:A,{x1}:] \/ [:B,{x2}:] c= proj2 f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in [:A,{x1}:] \/ [:B,{x2}:] )
A16: x1 in {x1} by TARSKI:def_1;
A17: x2 in {x2} by TARSKI:def_1;
assume  x in rng f ; ::_thesis: x in [:A,{x1}:] \/ [:B,{x2}:]
then consider y being set  such that
A18: y in dom f and
A19: x = f . y by FUNCT_1:def_3;
reconsider C = y as Ordinal by A1, A18;
percases ( y in A or not y in A ) ;
suppose y in A ; ::_thesis: x in [:A,{x1}:] \/ [:B,{x2}:]
then  ( x = [C,x1] & [C,x1] in [:A,{x1}:] ) by A1, A2, A18, A19, A16, ZFMISC_1:87;
hence  x in [:A,{x1}:] \/ [:B,{x2}:] by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA20: not y in A ; ::_thesis: x in [:A,{x1}:] \/ [:B,{x2}:]
then  A c= C by ORDINAL1:16;
then  A +^ (C -^ A) = C by ORDINAL3:def_5;
then  C -^ A in B by A1, A18, ORDINAL3:22;
then A21: [(C -^ A),x2] in [:B,{x2}:] by A17, ZFMISC_1:87;
 x = [(C -^ A),x2] by A1, A2, A18, A19, A20;
hence  x in [:A,{x1}:] \/ [:B,{x2}:] by A21, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:A,{x1}:] \/ [:B,{x2}:] or x in proj2 f )
assume A22: x in [:A,{x1}:] \/ [:B,{x2}:] ; ::_thesis: x in proj2 f
A23: now__::_thesis:_(_x_in_[:B,{x2}:]_implies_x_in_proj2_f_)
assume  x in [:B,{x2}:] ; ::_thesis: x in proj2 f
then consider y, z being set  such that
A24: y in B and
A25: z in {x2} and
A26: x = [y,z] by ZFMISC_1:84;
reconsider y = y as Ordinal by A24;
A27: A +^ y in A +^ B by A24, ORDINAL2:32;
A28: not A +^ y in A by ORDINAL1:5, ORDINAL3:24;
 ( (A +^ y) -^ A = y & z = x2 ) by A25, ORDINAL3:52, TARSKI:def_1;
then  x = f . (A +^ y) by A2, A26, A27, A28;
hence  x in proj2 f by A1, A27, FUNCT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x_in_[:A,{x1}:]_implies_x_in_proj2_f_)
assume  x in [:A,{x1}:] ; ::_thesis: x in proj2 f
then consider y, z being set  such that
A29: y in A and
A30: z in {x1} and
A31: x = [y,z] by ZFMISC_1:84;
A32: A c= A +^ B by ORDINAL3:24;
 z = x1 by A30, TARSKI:def_1;
then  x = f . y by A2, A29, A31, A32;
hence  x in proj2 f by A1, A29, A32, FUNCT_1:def_3; ::_thesis: verum
end;
hence  x in proj2 f by A22, A23, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) by CARD_1:5; ::_thesis: verum
end;

deffunc H2( set , set ) ->  set = [:$1,{0}:] \/ [:$2,{1}:];

Lm2:  for X, Y being set holds
( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
proof
let X, Y be set ; ::_thesis: ( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] )
deffunc H3( set ) ->  set = [($1 `2),($1 `1)];
consider f being Function such that
A1: ( dom f = [:X,Y:] & ( for x being set st x in [:X,Y:] holds
f . x = H3(x) ) ) from FUNCT_1:sch_3();
thus  [:X,Y:],[:Y,X:] are_equipotent ::_thesis: card [:X,Y:] = card [:Y,X:]
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = [:X,Y:] & proj2 f = [:Y,X:] )
thus  f is one-to-one ::_thesis: ( proj1 f = [:X,Y:] & proj2 f = [:Y,X:] )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume A2: ( x in dom f & y in dom f ) ; ::_thesis: ( not f . x = f . y or x = y )
then A3: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A1, MCART_1:21;
assume A4: f . x = f . y ; ::_thesis: x = y
A5: ( f . x = [(x `2),(x `1)] & f . y = [(y `2),(y `1)] ) by A1, A2;
then  x `1 = y `1 by A4, XTUPLE_0:1;
hence  x = y by A3, A5, A4, XTUPLE_0:1; ::_thesis: verum
end;
thus  dom f = [:X,Y:] by A1; ::_thesis: proj2 f = [:Y,X:]
thus  rng f c= [:Y,X:] :: according to XBOOLE_0:def_10 ::_thesis: [:Y,X:] c= proj2 f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in [:Y,X:] )
assume  x in rng f ; ::_thesis: x in [:Y,X:]
then consider y being set  such that
A6: y in dom f and
A7: x = f . y by FUNCT_1:def_3;
A8: y `2 in Y by A1, A6, MCART_1:10;
 ( x = [(y `2),(y `1)] & y `1 in X ) by A1, A6, A7, MCART_1:10;
hence  x in [:Y,X:] by A8, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:Y,X:] or x in proj2 f )
A9: ( [(x `2),(x `1)] `1 = x `2 & [(x `2),(x `1)] `2 = x `1 ) ;
assume A10: x in [:Y,X:] ; ::_thesis: x in proj2 f
then A11: x = [(x `1),(x `2)] by MCART_1:21;
A12: ( x `1 in Y & x `2 in X ) by A10, MCART_1:10;
then  [(x `2),(x `1)] in [:X,Y:] by ZFMISC_1:87;
then  f . [(x `2),(x `1)] in rng f by A1, FUNCT_1:def_3;
hence  x in proj2 f by A1, A11, A12, A9, ZFMISC_1:87; ::_thesis: verum
end;
hence  card [:X,Y:] = card [:Y,X:] by CARD_1:5; ::_thesis: verum
end;

definition
let M, N be Cardinal;
funcM +` N ->  Cardinal equals :: CARD_2:def 1
 card (M +^ N);
coherence
 card (M +^ N) is Cardinal ;
commutativity
 for b1, M, N being Cardinal st b1 = card (M +^ N) holds
b1 = card (N +^ M)
proof
let C, M, N be Cardinal; ::_thesis: ( C = card (M +^ N) implies C = card (N +^ M) )
assume  C = card (M +^ N) ; ::_thesis: C = card (N +^ M)
hence C = card H2(N,M) by Lm1
.= card (N +^ M) by Lm1 ;
::_thesis: verum
end;
funcM *` N ->  Cardinal equals :: CARD_2:def 2
 card [:M,N:];
coherence
 card [:M,N:] is Cardinal ;
commutativity
 for b1, M, N being Cardinal st b1 = card [:M,N:] holds
b1 = card [:N,M:] by Lm2;
func exp (M,N) ->  Cardinal equals :: CARD_2:def 3
 card (Funcs (N,M));
coherence
 card (Funcs (N,M)) is Cardinal ;
end;

:: deftheorem  defines +` CARD_2:def_1_:_
 for M, N being Cardinal holds M +` N = card (M +^ N);

:: deftheorem  defines *` CARD_2:def_2_:_
 for M, N being Cardinal holds M *` N = card [:M,N:];

:: deftheorem  defines exp CARD_2:def_3_:_
 for M, N being Cardinal holds exp (M,N) = card (Funcs (N,M));

theorem Th4: :: CARD_2:4
for X, Y being set holds
( [:X,Y:],[:Y,X:] are_equipotent & card [:X,Y:] = card [:Y,X:] ) by Lm2;

theorem Th5: :: CARD_2:5
for X, Y, Z being set holds
( [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )
proof
let X, Y, Z be set ; ::_thesis: ( [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent & card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] )
deffunc H3( set ) ->  set = [(($1 `1) `1),[(($1 `1) `2),($1 `2)]];
consider f being Function such that
A1: ( dom f = [:[:X,Y:],Z:] & ( for x being set st x in [:[:X,Y:],Z:] holds
f . x = H3(x) ) ) from FUNCT_1:sch_3();
thus  [:[:X,Y:],Z:],[:X,[:Y,Z:]:] are_equipotent ::_thesis: card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:]
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = [:[:X,Y:],Z:] & proj2 f = [:X,[:Y,Z:]:] )
thus  f is one-to-one ::_thesis: ( proj1 f = [:[:X,Y:],Z:] & proj2 f = [:X,[:Y,Z:]:] )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A2: x in dom f and
A3: y in dom f ; ::_thesis: ( not f . x = f . y or x = y )
assume A4: f . x = f . y ; ::_thesis: x = y
A5: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A1, A2, A3, MCART_1:21;
 x `1 in [:X,Y:] by A1, A2, MCART_1:10;
then A6: x `1 = [((x `1) `1),((x `1) `2)] by MCART_1:21;
A7: ( f . x = [((x `1) `1),[((x `1) `2),(x `2)]] & f . y = [((y `1) `1),[((y `1) `2),(y `2)]] ) by A1, A2, A3;
then A8: (x `1) `1 = (y `1) `1 by A4, XTUPLE_0:1;
 y `1 in [:X,Y:] by A1, A3, MCART_1:10;
then A9: y `1 = [((y `1) `1),((y `1) `2)] by MCART_1:21;
A10: [((x `1) `2),(x `2)] = [((y `1) `2),(y `2)] by A7, A4, XTUPLE_0:1;
then  (x `1) `2 = (y `1) `2 by XTUPLE_0:1;
hence  x = y by A5, A8, A10, A6, A9, XTUPLE_0:1; ::_thesis: verum
end;
thus  dom f = [:[:X,Y:],Z:] by A1; ::_thesis: proj2 f = [:X,[:Y,Z:]:]
thus  rng f c= [:X,[:Y,Z:]:] :: according to XBOOLE_0:def_10 ::_thesis: [:X,[:Y,Z:]:] c= proj2 f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in [:X,[:Y,Z:]:] )
assume  x in rng f ; ::_thesis: x in [:X,[:Y,Z:]:]
then consider y being set  such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def_3;
A13: y `1 in [:X,Y:] by A1, A11, MCART_1:10;
then A14: (y `1) `2 in Y by MCART_1:10;
 y `2 in Z by A1, A11, MCART_1:10;
then A15: [((y `1) `2),(y `2)] in [:Y,Z:] by A14, ZFMISC_1:87;
A16: (y `1) `1 in X by A13, MCART_1:10;
 x = [((y `1) `1),[((y `1) `2),(y `2)]] by A1, A11, A12;
hence  x in [:X,[:Y,Z:]:] by A16, A15, ZFMISC_1:87; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:X,[:Y,Z:]:] or x in proj2 f )
A17: ( [(x `1),((x `2) `1)] `1 = x `1 & [(x `1),((x `2) `1)] `2 = (x `2) `1 ) ;
A18: ( [[(x `1),((x `2) `1)],((x `2) `2)] `1 = [(x `1),((x `2) `1)] & [[(x `1),((x `2) `1)],((x `2) `2)] `2 = (x `2) `2 ) ;
assume A19: x in [:X,[:Y,Z:]:] ; ::_thesis: x in proj2 f
then A20: x `2 in [:Y,Z:] by MCART_1:10;
then A21: (x `2) `1 in Y by MCART_1:10;
A22: (x `2) `2 in Z by A20, MCART_1:10;
 x `1 in X by A19, MCART_1:10;
then A23: [(x `1),((x `2) `1)] in [:X,Y:] by A21, ZFMISC_1:87;
then A24: [[(x `1),((x `2) `1)],((x `2) `2)] in [:[:X,Y:],Z:] by A22, ZFMISC_1:87;
A25: x `2 = [((x `2) `1),((x `2) `2)] by A20, MCART_1:21;
 x = [(x `1),(x `2)] by A19, MCART_1:21;
then  x = f . [[(x `1),((x `2) `1)],((x `2) `2)] by A1, A25, A17, A23, A18, A22, ZFMISC_1:87;
hence  x in proj2 f by A1, A24, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card [:[:X,Y:],Z:] = card [:X,[:Y,Z:]:] by CARD_1:5; ::_thesis: verum
end;

theorem Th6: :: CARD_2:6
for X, x being set holds
( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
proof
let X, x be set ; ::_thesis: ( X,[:X,{x}:] are_equipotent & card X = card [:X,{x}:] )
deffunc H3( set ) ->  set = [$1,x];
consider f being Function such that
A1: ( dom f = X & ( for y being set st y in X holds
f . y = H3(y) ) ) from FUNCT_1:sch_3();
thus  X,[:X,{x}:] are_equipotent ::_thesis: card X = card [:X,{x}:]
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = X & proj2 f = [:X,{x}:] )
thus  f is one-to-one ::_thesis: ( proj1 f = X & proj2 f = [:X,{x}:] )
proof
let y be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not y in proj1 f or not b1 in proj1 f or not f . y = f . b1 or y = b1 )
let z be set ; ::_thesis: ( not y in proj1 f or not z in proj1 f or not f . y = f . z or y = z )
assume that
A2: ( y in dom f & z in dom f ) and
A3: f . y = f . z ; ::_thesis: y = z
A4: [y,x] `1 = y ;
 ( f . y = [y,x] & f . z = [z,x] ) by A1, A2;
hence  y = z by A3, A4, MCART_1:7; ::_thesis: verum
end;
thus  dom f = X by A1; ::_thesis: proj2 f = [:X,{x}:]
thus  rng f c= [:X,{x}:] :: according to XBOOLE_0:def_10 ::_thesis: [:X,{x}:] c= proj2 f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in [:X,{x}:] )
A5: x in {x} by TARSKI:def_1;
assume  y in rng f ; ::_thesis: y in [:X,{x}:]
then consider z being set  such that
A6: z in dom f and
A7: y = f . z by FUNCT_1:def_3;
 y = [z,x] by A1, A6, A7;
hence  y in [:X,{x}:] by A1, A6, A5, ZFMISC_1:87; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:X,{x}:] or y in proj2 f )
assume  y in [:X,{x}:] ; ::_thesis: y in proj2 f
then consider y1, y2 being set  such that
A8: y1 in X and
A9: y2 in {x} and
A10: y = [y1,y2] by ZFMISC_1:84;
 y2 = x by A9, TARSKI:def_1;
then  y = f . y1 by A1, A8, A10;
hence  y in proj2 f by A1, A8, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card X = card [:X,{x}:] by CARD_1:5; ::_thesis: verum
end;

Lm3:  for X, Y being set holds [:X,Y:],[:(card X),Y:] are_equipotent
proof
let X, Y be set ; ::_thesis: [:X,Y:],[:(card X),Y:] are_equipotent
consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by CARD_1:def_2, WELLORD2:def_4;
deffunc H3( set ) ->  set = [(f . ($1 `1)),($1 `2)];
consider g being Function such that
A4: ( dom g = [:X,Y:] & ( for x being set st x in [:X,Y:] holds
g . x = H3(x) ) ) from FUNCT_1:sch_3();
take  g ; :: according to WELLORD2:def_4 ::_thesis: ( g is one-to-one & proj1 g = [:X,Y:] & proj2 g = [:(card X),Y:] )
thus  g is one-to-one ::_thesis: ( proj1 g = [:X,Y:] & proj2 g = [:(card X),Y:] )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 g or not b1 in proj1 g or not g . x = g . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 g or not y in proj1 g or not g . x = g . y or x = y )
assume A5: ( x in dom g & y in dom g ) ; ::_thesis: ( not g . x = g . y or x = y )
then A6: ( x `1 in X & y `1 in X ) by A4, MCART_1:10;
assume A7: g . x = g . y ; ::_thesis: x = y
 ( g . x = [(f . (x `1)),(x `2)] & g . y = [(f . (y `1)),(y `2)] ) by A4, A5;
then A8: ( f . (x `1) = f . (y `1) & x `2 = y `2 ) by A7, XTUPLE_0:1;
 ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A4, A5, MCART_1:21;
hence  x = y by A1, A2, A6, A8, FUNCT_1:def_4; ::_thesis: verum
end;
thus  dom g = [:X,Y:] by A4; ::_thesis: proj2 g = [:(card X),Y:]
thus  rng g c= [:(card X),Y:] :: according to XBOOLE_0:def_10 ::_thesis: [:(card X),Y:] c= proj2 g
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in [:(card X),Y:] )
assume  y in rng g ; ::_thesis: y in [:(card X),Y:]
then consider x being set  such that
A9: x in dom g and
A10: y = g . x by FUNCT_1:def_3;
 x `1 in X by A4, A9, MCART_1:10;
then A11: f . (x `1) in card X by A2, A3, FUNCT_1:def_3;
 ( y = [(f . (x `1)),(x `2)] & x `2 in Y ) by A4, A9, A10, MCART_1:10;
hence  y in [:(card X),Y:] by A11, ZFMISC_1:87; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [:(card X),Y:] or y in proj2 g )
assume A12: y in [:(card X),Y:] ; ::_thesis: y in proj2 g
then  y `1 in card X by MCART_1:10;
then consider x being set  such that
A13: x in X and
A14: y `1 = f . x by A2, A3, FUNCT_1:def_3;
A15: y = [(y `1),(y `2)] by A12, MCART_1:21;
A16: y `2 in Y by A12, MCART_1:10;
then A17: [x,(y `2)] in [:X,Y:] by A13, ZFMISC_1:87;
 ( [x,(y `2)] `1 = x & [x,(y `2)] `2 = y `2 ) ;
then  g . [x,(y `2)] = y by A4, A15, A14, A16, A13, ZFMISC_1:87;
hence  y in proj2 g by A4, A17, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th7: :: CARD_2:7
for X, Y being set holds
( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent & [:X,Y:],[:(card X),(card Y):] are_equipotent & card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
proof
let X, Y be set ; ::_thesis: ( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent & [:X,Y:],[:(card X),(card Y):] are_equipotent & card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
 ( [:Y,X:],[:(card Y),X:] are_equipotent & [:X,Y:],[:Y,X:] are_equipotent ) by Lm2, Lm3;
then A1: [:X,Y:],[:(card Y),X:] are_equipotent by WELLORD2:15;
A2: [:(card Y),X:],[:X,(card Y):] are_equipotent by Lm2;
hence A3: ( [:X,Y:],[:(card X),Y:] are_equipotent & [:X,Y:],[:X,(card Y):] are_equipotent ) by A1, Lm3, WELLORD2:15; ::_thesis: ( [:X,Y:],[:(card X),(card Y):] are_equipotent & card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
 [:X,(card Y):],[:(card X),(card Y):] are_equipotent by Lm3;
hence  [:X,Y:],[:(card X),(card Y):] are_equipotent by A3, WELLORD2:15; ::_thesis: ( card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] )
hence  ( card [:X,Y:] = card [:(card X),Y:] & card [:X,Y:] = card [:X,(card Y):] & card [:X,Y:] = card [:(card X),(card Y):] ) by A2, A1, Lm3, CARD_1:5, WELLORD2:15; ::_thesis: verum
end;

theorem Th8: :: CARD_2:8
for X1, Y1, X2, Y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent holds
( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] )
proof
let X1, Y1, X2, Y2 be set ; ::_thesis: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent implies ( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] ) )
assume  ( X1,Y1 are_equipotent & X2,Y2 are_equipotent ) ; ::_thesis: ( [:X1,X2:],[:Y1,Y2:] are_equipotent & card [:X1,X2:] = card [:Y1,Y2:] )
then A1: ( card X1 = card Y1 & card X2 = card Y2 ) by CARD_1:5;
 ( [:X1,X2:],[:(card X1),(card X2):] are_equipotent & [:Y1,Y2:],[:(card Y1),(card Y2):] are_equipotent ) by Th7;
hence  [:X1,X2:],[:Y1,Y2:] are_equipotent by A1, WELLORD2:15; ::_thesis: card [:X1,X2:] = card [:Y1,Y2:]
hence  card [:X1,X2:] = card [:Y1,Y2:] by CARD_1:5; ::_thesis: verum
end;

theorem :: CARD_2:9
for A, B being Ordinal
for x1, x2 being set st x1 <> x2 holds
( A +^ B,[:A,{x1}:] \/ [:B,{x2}:] are_equipotent & card (A +^ B) = card ([:A,{x1}:] \/ [:B,{x2}:]) ) by Lm1;

theorem Th10: :: CARD_2:10
for K, M being Cardinal
for x1, x2 being set st x1 <> x2 holds
( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )
proof
let K, M be Cardinal; ::_thesis: for x1, x2 being set st x1 <> x2 holds
( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )
let x1, x2 be set ; ::_thesis: ( x1 <> x2 implies ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) ) )
assume  x1 <> x2 ; ::_thesis: ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) )
then  card ([:K,{x1}:] \/ [:M,{x2}:]) = K +` M by Lm1;
hence  ( K +` M,[:K,{x1}:] \/ [:M,{x2}:] are_equipotent & K +` M = card ([:K,{x1}:] \/ [:M,{x2}:]) ) by CARD_1:def_2; ::_thesis: verum
end;

theorem Th11: :: CARD_2:11
for A, B being Ordinal holds
( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )
proof
let A, B be Ordinal; ::_thesis: ( A *^ B,[:A,B:] are_equipotent & card (A *^ B) = card [:A,B:] )
defpred S1[ set , set ] means  ex O1, O2 being Ordinal st
( O1 = $1 `1 & O2 = $1 `2 & $2 = (O1 *^ B) +^ O2 );
A1: for x being set st x in [:A,B:] holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in [:A,B:] implies ex y being set st S1[x,y] )
assume  x in [:A,B:] ; ::_thesis: ex y being set st S1[x,y]
then  ( x `1 in A & x `2 in B ) by MCART_1:10;
then reconsider x1 = x `1 , x2 = x `2 as Ordinal ;
take  (x1 *^ B) +^ x2 ; ::_thesis: S1[x,(x1 *^ B) +^ x2]
take  x1 ; ::_thesis: ex O2 being Ordinal st
( x1 = x `1 & O2 = x `2 & (x1 *^ B) +^ x2 = (x1 *^ B) +^ O2 )
take  x2 ; ::_thesis: ( x1 = x `1 & x2 = x `2 & (x1 *^ B) +^ x2 = (x1 *^ B) +^ x2 )
thus  ( x1 = x `1 & x2 = x `2 & (x1 *^ B) +^ x2 = (x1 *^ B) +^ x2 ) ; ::_thesis: verum
end;
consider f being Function such that
A2: ( dom f = [:A,B:] & ( for x being set st x in [:A,B:] holds
S1[x,f . x] ) ) from CLASSES1:sch_1(A1);
A3: [:A,B:],A *^ B are_equipotent
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = [:A,B:] & proj2 f = A *^ B )
thus  f is one-to-one ::_thesis: ( proj1 f = [:A,B:] & proj2 f = A *^ B )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in proj1 f or not b1 in proj1 f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume A4: ( x in dom f & y in dom f ) ; ::_thesis: ( not f . x = f . y or x = y )
then A5: ( x `2 in B & y `2 in B ) by A2, MCART_1:10;
 ( x `1 in A & y `1 in A ) by A2, A4, MCART_1:10;
then reconsider x1 = x `1 , y1 = y `1 as Ordinal ;
assume A6: f . x = f . y ; ::_thesis: x = y
A7: ( x = [(x `1),(x `2)] & y = [(y `1),(y `2)] ) by A2, A4, MCART_1:21;
A8: ( ex O1, O2 being Ordinal st
( O1 = x `1 & O2 = x `2 & f . x = (O1 *^ B) +^ O2 ) & ex O3, O4 being Ordinal st
( O3 = y `1 & O4 = y `2 & f . y = (O3 *^ B) +^ O4 ) ) by A2, A4;
then  x1 = y1 by A5, A6, ORDINAL3:48;
hence  x = y by A7, A5, A8, A6, ORDINAL3:48; ::_thesis: verum
end;
thus  dom f = [:A,B:] by A2; ::_thesis: proj2 f = A *^ B
thus  rng f c= A *^ B :: according to XBOOLE_0:def_10 ::_thesis: A *^ B c= proj2 f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in A *^ B )
A9: 1 *^ B = B by ORDINAL2:39;
assume  y in rng f ; ::_thesis: y in A *^ B
then consider x being set  such that
A10: x in dom f and
A11: y = f . x by FUNCT_1:def_3;
consider x1, x2 being Ordinal such that
A12: x1 = x `1 and
A13: ( x2 = x `2 & f . x = (x1 *^ B) +^ x2 ) by A2, A10;
 x1 +^ 1 = succ x1 by ORDINAL2:31;
then A14: (x1 *^ B) +^ (1 *^ B) = (succ x1) *^ B by ORDINAL3:46;
 succ x1 c= A by A12, A2, A10, MCART_1:10, ORDINAL1:21;
then A15: (x1 *^ B) +^ (1 *^ B) c= A *^ B by A14, ORDINAL2:41;
 y in (x1 *^ B) +^ (1 *^ B) by A11, A13, A9, A2, A10, MCART_1:10, ORDINAL2:32;
hence  y in A *^ B by A15; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A *^ B or y in proj2 f )
assume A16: y in A *^ B ; ::_thesis: y in proj2 f
then reconsider C = y as Ordinal ;
A17: ( C = ((C div^ B) *^ B) +^ (C mod^ B) & [(C div^ B),(C mod^ B)] `1 = C div^ B ) by ORDINAL3:65;
 ( C div^ B in A & C mod^ B in B ) by A16, ORDINAL3:67;
then A18: [(C div^ B),(C mod^ B)] in [:A,B:] by ZFMISC_1:87;
then  ( [(C div^ B),(C mod^ B)] `2 = C mod^ B & ex O1, O2 being Ordinal st
( O1 = [(C div^ B),(C mod^ B)] `1 & O2 = [(C div^ B),(C mod^ B)] `2 & f . [(C div^ B),(C mod^ B)] = (O1 *^ B) +^ O2 ) ) by A2;
hence  y in proj2 f by A2, A18, A17, FUNCT_1:def_3; ::_thesis: verum
end;
hence  A *^ B,[:A,B:] are_equipotent ; ::_thesis: card (A *^ B) = card [:A,B:]
thus  card (A *^ B) = card [:A,B:] by A3, CARD_1:5; ::_thesis: verum
end;

deffunc H3( set , set ) ->  set = [:$1,{0}:] \/ [:$2,{1}:];

deffunc H4( set , set , set , set ) ->  set = [:$1,{$3}:] \/ [:$2,{$4}:];

theorem Th12: :: CARD_2:12
for X1, Y1, X2, Y2, x1, x2, y1, y2 being set st X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 holds
( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
proof
let X1, Y1, X2, Y2, x1, x2, y1, y2 be set ; ::_thesis: ( X1,Y1 are_equipotent & X2,Y2 are_equipotent & x1 <> x2 & y1 <> y2 implies ( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) ) )
assume that
A1: X1,Y1 are_equipotent and
A2: X2,Y2 are_equipotent and
A3: x1 <> x2 and
A4: y1 <> y2 ; ::_thesis: ( [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent & card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) )
 {x2},{y2} are_equipotent by CARD_1:28;
then A5: [:X2,{x2}:],[:Y2,{y2}:] are_equipotent by A2, Th8;
A6: now__::_thesis:_not_[:Y1,{y1}:]_meets_[:Y2,{y2}:]
assume  [:Y1,{y1}:] meets [:Y2,{y2}:] ; ::_thesis: contradiction
then consider y being set  such that
A7: y in [:Y1,{y1}:] and
A8: y in [:Y2,{y2}:] by XBOOLE_0:3;
 y `2 in {y1} by A7, MCART_1:10;
then A9: y `2 = y1 by TARSKI:def_1;
 y `2 in {y2} by A8, MCART_1:10;
hence  contradiction by A4, A9, TARSKI:def_1; ::_thesis: verum
end;
A10: now__::_thesis:_not_[:X1,{x1}:]_meets_[:X2,{x2}:]
assume  [:X1,{x1}:] meets [:X2,{x2}:] ; ::_thesis: contradiction
then consider x being set  such that
A11: x in [:X1,{x1}:] and
A12: x in [:X2,{x2}:] by XBOOLE_0:3;
 x `2 in {x1} by A11, MCART_1:10;
then A13: x `2 = x1 by TARSKI:def_1;
 x `2 in {x2} by A12, MCART_1:10;
hence  contradiction by A3, A13, TARSKI:def_1; ::_thesis: verum
end;
 {x1},{y1} are_equipotent by CARD_1:28;
then  [:X1,{x1}:],[:Y1,{y1}:] are_equipotent by A1, Th8;
hence  [:X1,{x1}:] \/ [:X2,{x2}:],[:Y1,{y1}:] \/ [:Y2,{y2}:] are_equipotent by A5, A10, A6, CARD_1:31; ::_thesis: card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:])
hence  card ([:X1,{x1}:] \/ [:X2,{x2}:]) = card ([:Y1,{y1}:] \/ [:Y2,{y2}:]) by CARD_1:5; ::_thesis: verum
end;

theorem Th13: :: CARD_2:13
for A, B being Ordinal holds card (A +^ B) = (card A) +` (card B)
proof
let A, B be Ordinal; ::_thesis: card (A +^ B) = (card A) +` (card B)
A1: A +^ B,H3(A,B) are_equipotent by Lm1;
 ( A, card A are_equipotent & B, card B are_equipotent ) by CARD_1:def_2;
then A2: H3(A,B),H3( card A, card B) are_equipotent by Th12;
 H3( card A, card B),(card A) +^ (card B) are_equipotent by Lm1;
then  H3(A,B),(card A) +^ (card B) are_equipotent by A2, WELLORD2:15;
then  A +^ B,(card A) +^ (card B) are_equipotent by A1, WELLORD2:15;
hence  card (A +^ B) = (card A) +` (card B) by CARD_1:5; ::_thesis: verum
end;

theorem Th14: :: CARD_2:14
for A, B being Ordinal holds card (A *^ B) = (card A) *` (card B)
proof
let A, B be Ordinal; ::_thesis: card (A *^ B) = (card A) *` (card B)
thus  card (A *^ B) = card [:A,B:] by Th11
.= (card A) *` (card B) by Th7 ; ::_thesis: verum
end;

theorem :: CARD_2:15
for X, Y being set holds
( [:X,{0}:] \/ [:Y,{1}:],[:Y,{0}:] \/ [:X,{1}:] are_equipotent & card ([:X,{0}:] \/ [:Y,{1}:]) = card ([:Y,{0}:] \/ [:X,{1}:]) ) by Th12;

theorem Th16: :: CARD_2:16
for X1, X2, Y1, Y2 being set holds
( [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )
proof
let X1, X2, Y1, Y2 be set ; ::_thesis: ( [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent & card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) )
deffunc H5( set ) ->  set = [($1 `2),($1 `1)];
consider f being Function such that
A1: ( dom f = [:X1,X2:] \/ [:Y1,Y2:] & ( for x being set st x in [:X1,X2:] \/ [:Y1,Y2:] holds
f . x = H5(x) ) ) from FUNCT_1:sch_3();
thus  [:X1,X2:] \/ [:Y1,Y2:],[:X2,X1:] \/ [:Y2,Y1:] are_equipotent ::_thesis: card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:])
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & proj1 f = [:X1,X2:] \/ [:Y1,Y2:] & proj2 f = [:X2,X1:] \/ [:Y2,Y1:] )
thus  f is one-to-one ::_thesis: ( proj1 f = [:X1,X2:] \/ [:Y1,Y2:] & proj2 f = [:X2,X1:] \/ [:Y2,Y1:] )
proof
let x1 be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x1 in proj1 f or not b1 in proj1 f or not f . x1 = f . b1 or x1 = b1 )
let x2 be set ; ::_thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f . x1 = f . x2 ; ::_thesis: x1 = x2
 ( x1 in [:X1,X2:] or x1 in [:Y1,Y2:] ) by A1, A2, XBOOLE_0:def_3;
then A5: x1 = [(x1 `1),(x1 `2)] by MCART_1:21;
 ( x2 in [:X1,X2:] or x2 in [:Y1,Y2:] ) by A1, A3, XBOOLE_0:def_3;
then A6: x2 = [(x2 `1),(x2 `2)] by MCART_1:21;
A7: ( f . x1 = [(x1 `2),(x1 `1)] & f . x2 = [(x2 `2),(x2 `1)] ) by A1, A2, A3;
then  x1 `1 = x2 `1 by A4, XTUPLE_0:1;
hence  x1 = x2 by A4, A7, A5, A6, XTUPLE_0:1; ::_thesis: verum
end;
thus  dom f = [:X1,X2:] \/ [:Y1,Y2:] by A1; ::_thesis: proj2 f = [:X2,X1:] \/ [:Y2,Y1:]
thus  rng f c= [:X2,X1:] \/ [:Y2,Y1:] :: according to XBOOLE_0:def_10 ::_thesis: [:X2,X1:] \/ [:Y2,Y1:] c= proj2 f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in [:X2,X1:] \/ [:Y2,Y1:] )
assume  x in rng f ; ::_thesis: x in [:X2,X1:] \/ [:Y2,Y1:]
then consider y being set  such that
A8: y in dom f and
A9: x = f . y by FUNCT_1:def_3;
 ( y in [:X1,X2:] or y in [:Y1,Y2:] ) by A1, A8, XBOOLE_0:def_3;
then A10: ( ( y `1 in X1 & y `2 in X2 ) or ( y `1 in Y1 & y `2 in Y2 ) ) by MCART_1:10;
 x = [(y `2),(y `1)] by A1, A8, A9;
then  ( x in [:X2,X1:] or x in [:Y2,Y1:] ) by A10, ZFMISC_1:87;
hence  x in [:X2,X1:] \/ [:Y2,Y1:] by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [:X2,X1:] \/ [:Y2,Y1:] or x in proj2 f )
A11: ( [(x `2),(x `1)] `1 = x `2 & [(x `2),(x `1)] `2 = x `1 ) ;
assume  x in [:X2,X1:] \/ [:Y2,Y1:] ; ::_thesis: x in proj2 f
then A12: ( x in [:X2,X1:] or x in [:Y2,Y1:] ) by XBOOLE_0:def_3;
then  ( ( x `1 in X2 & x `2 in X1 ) or ( x `1 in Y2 & x `2 in Y1 ) ) by MCART_1:10;
then  ( [(x `2),(x `1)] in [:X1,X2:] or [(x `2),(x `1)] in [:Y1,Y2:] ) by ZFMISC_1:87;
then A13: [(x `2),(x `1)] in [:X1,X2:] \/ [:Y1,Y2:] by XBOOLE_0:def_3;
 x = [(x `1),(x `2)] by A12, MCART_1:21;
then  f . [(x `2),(x `1)] = x by A1, A13, A11;
hence  x in proj2 f by A1, A13, FUNCT_1:def_3; ::_thesis: verum
end;
hence  card ([:X1,X2:] \/ [:Y1,Y2:]) = card ([:X2,X1:] \/ [:Y2,Y1:]) by CARD_1:5; ::_thesis: verum
end;

theorem Th17: :: CARD_2:17
for x, y, X, Y being set st x <> y holds
(card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
proof
let x, y, X, Y be set ; ::_thesis: ( x <> y implies (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) )
assume A1: x <> y ; ::_thesis: (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:])
 ( X, card X are_equipotent & Y, card Y are_equipotent ) by CARD_1:def_2;
then  card H4(X,Y,x,y) = card H4( card X, card Y,x,y) by A1, Th12;
hence  (card X) +` (card Y) = card ([:X,{x}:] \/ [:Y,{y}:]) by A1, Lm1; ::_thesis: verum
end;

theorem :: CARD_2:18
for M being Cardinal holds M +` 0 = M
proof
let M be Cardinal; ::_thesis: M +` 0 = M
thus M +` 0 = card H3(M, {} ) by Lm1
.= card M by Th6
.= M by CARD_1:def_2 ; ::_thesis: verum
end;

Lm4:  for x, y, X, Y being set st x <> y holds
[:X,{x}:] misses [:Y,{y}:]
proof
let x, y, X, Y be set ; ::_thesis: ( x <> y implies [:X,{x}:] misses [:Y,{y}:] )
assume A1: x <> y ; ::_thesis: [:X,{x}:] misses [:Y,{y}:]
assume  not [:X,{x}:] misses [:Y,{y}:] ; ::_thesis: contradiction
then consider z being set  such that
A2: z in [:X,{x}:] and
A3: z in [:Y,{y}:] by XBOOLE_0:3;
 z `2 = x by A2, MCART_1:13;
hence  contradiction by A1, A3, MCART_1:13; ::_thesis: verum
end;

theorem Th19: :: CARD_2:19
for K, M, N being Cardinal holds (K +` M) +` N = K +` (M +` N)
proof
let K, M, N be Cardinal; ::_thesis: (K +` M) +` N = K +` (M +` N)
A1: card ((K +` M) +` N) = (K +` M) +` N ;
A2: (K +` M) +` N,[:(K +` M),{0}:] \/ [:N,{2}:] are_equipotent by Th10;
 [:M,{1}:] misses [:N,{2}:] by Lm4;
then A3: [:M,{1}:] /\ [:N,{2}:] = {} by XBOOLE_0:def_7;
 [:K,{0}:] misses [:N,{2}:] by Lm4;
then  [:K,{0}:] /\ [:N,{2}:] = {} by XBOOLE_0:def_7;
then ([:K,{0}:] \/ [:M,{1}:]) /\ [:N,{2}:] = {} \/ {} by A3, XBOOLE_1:23
.= {} ;
then A4: [:K,{0}:] \/ [:M,{1}:] misses [:N,{2}:] by XBOOLE_0:def_7;
 ( K +` M,[:K,{0}:] \/ [:M,{1}:] are_equipotent & K +` M,[:(K +` M),{0}:] are_equipotent ) by Th6, Th10;
then A5: [:(K +` M),{0}:],[:K,{0}:] \/ [:M,{1}:] are_equipotent by WELLORD2:15;
 [:K,{0}:] misses [:N,{2}:] by Lm4;
then A6: [:K,{0}:] /\ [:N,{2}:] = {} by XBOOLE_0:def_7;
 [:K,{0}:] misses [:M,{1}:] by Lm4;
then  [:K,{0}:] /\ [:M,{1}:] = {} by XBOOLE_0:def_7;
then [:K,{0}:] /\ ([:M,{1}:] \/ [:N,{2}:]) = {} \/ {} by A6, XBOOLE_1:23
.= {} ;
then A7: [:K,{0}:] misses [:M,{1}:] \/ [:N,{2}:] by XBOOLE_0:def_7;
 ( M +` N,[:M,{1}:] \/ [:N,{2}:] are_equipotent & M +` N,[:(M +` N),{2}:] are_equipotent ) by Th6, Th10;
then A8: [:(M +` N),{2}:],[:M,{1}:] \/ [:N,{2}:] are_equipotent by WELLORD2:15;
 [:K,{0}:] misses [:(M +` N),{2}:] by Lm4;
then A9: [:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]),[:K,{0}:] \/ [:(M +` N),{2}:] are_equipotent by A7, A8, CARD_1:31;
 [:(K +` M),{0}:] misses [:N,{2}:] by Lm4;
then A10: [:(K +` M),{0}:] \/ [:N,{2}:],([:K,{0}:] \/ [:M,{1}:]) \/ [:N,{2}:] are_equipotent by A4, A5, CARD_1:31;
 [:K,{0}:] \/ ([:M,{1}:] \/ [:N,{2}:]) = ([:K,{0}:] \/ [:M,{1}:]) \/ [:N,{2}:] by XBOOLE_1:4;
then  [:(K +` M),{0}:] \/ [:N,{2}:],[:K,{0}:] \/ [:(M +` N),{2}:] are_equipotent by A10, A9, WELLORD2:15;
then A11: (K +` M) +` N,[:K,{0}:] \/ [:(M +` N),{2}:] are_equipotent by A2, WELLORD2:15;
 [:K,{0}:] \/ [:(M +` N),{2}:],K +` (M +` N) are_equipotent by Th10;
then  (K +` M) +` N,K +` (M +` N) are_equipotent by A11, WELLORD2:15;
hence  (K +` M) +` N = K +` (M +` N) by A1, CARD_1:def_2; ::_thesis: verum
end;

theorem :: CARD_2:20
for K being Cardinal holds K *` 0 = 0 ;

theorem Th21: :: CARD_2:21
for K being Cardinal holds K *` 1 = K
proof
let K be Cardinal; ::_thesis: K *` 1 = K
 K = card K by CARD_1:def_2;
hence  K *` 1 = K by Th6, ORDINAL3:15; ::_thesis: verum
end;

theorem Th22: :: CARD_2:22
for K, M, N being Cardinal holds (K *` M) *` N = K *` (M *` N)
proof
let K, M, N be Cardinal; ::_thesis: (K *` M) *` N = K *` (M *` N)
thus (K *` M) *` N = card [:[:K,M:],N:] by Th7
.= card [:K,[:M,N:]:] by Th5
.= K *` (M *` N) by Th7 ; ::_thesis: verum
end;

theorem Th23: :: CARD_2:23
for K being Cardinal holds 2 *` K = K +` K
proof
let K be Cardinal; ::_thesis: 2 *` K = K +` K
thus 2 *` K = card ([:{{}},K:] \/ [:{1},K:]) by CARD_1:50, ZFMISC_1:109
.= card ([:K,{{}}:] \/ [:K,{1}:]) by Th16
.= (card K) +` (card K) by Th17
.= K +` (card K) by CARD_1:def_2
.= K +` K by CARD_1:def_2 ; ::_thesis: verum
end;

theorem Th24: :: CARD_2:24
for K, M, N being Cardinal holds K *` (M +` N) = (K *` M) +` (K *` N)
proof
let K, M, N be Cardinal; ::_thesis: K *` (M +` N) = (K *` M) +` (K *` N)
A1: [:(card [:K,M:]),{0}:],[:[:K,M:],{0}:] are_equipotent by Th7;
 M,[:M,{0}:] are_equipotent by Th6;
then A2: [:K,M:],[:K,[:M,{0}:]:] are_equipotent by Th8;
 [:[:K,M:],{0}:],[:K,M:] are_equipotent by Th6;
then  [:[:K,M:],{0}:],[:K,[:M,{0}:]:] are_equipotent by A2, WELLORD2:15;
then A3: [:(card [:K,M:]),{0}:],[:K,[:M,{0}:]:] are_equipotent by A1, WELLORD2:15;
A4: [:(card [:K,N:]),{1}:],[:[:K,N:],{1}:] are_equipotent by Th7;
 [:M,{0}:] misses [:N,{1}:] by Lm4;
then A5: [:K,[:M,{0}:]:] misses [:K,[:N,{1}:]:] by ZFMISC_1:104;
 N,[:N,{1}:] are_equipotent by Th6;
then A6: [:K,N:],[:K,[:N,{1}:]:] are_equipotent by Th8;
A7: K *` (M +` N) = card [:K,(card H3(M,N)):] by Th10
.= card [:K,H3(M,N):] by Th7
.= card ([:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:]) by ZFMISC_1:97 ;
 [:[:K,N:],{1}:],[:K,N:] are_equipotent by Th6;
then  [:[:K,N:],{1}:],[:K,[:N,{1}:]:] are_equipotent by A6, WELLORD2:15;
then A8: [:(card [:K,N:]),{1}:],[:K,[:N,{1}:]:] are_equipotent by A4, WELLORD2:15;
 [:(card [:K,M:]),{0}:] misses [:(card [:K,N:]),{1}:] by Lm4;
then  [:(card [:K,M:]),{0}:] \/ [:(card [:K,N:]),{1}:],[:K,[:M,{0}:]:] \/ [:K,[:N,{1}:]:] are_equipotent by A3, A8, A5, CARD_1:31;
hence K *` (M +` N) = card ([:(card [:K,M:]),{0}:] \/ [:(card [:K,N:]),{1}:]) by A7, CARD_1:5
.= (K *` M) +` (K *` N) by Th10 ;
::_thesis: verum
end;

theorem :: CARD_2:25
for K being Cardinal holds exp (K,0) = 1
proof
let K be Cardinal; ::_thesis: exp (K,0) = 1
thus  exp (K,0) = card {{}} by FUNCT_5:57
.= 1 by CARD_1:30 ; ::_thesis: verum
end;

theorem :: CARD_2:26
for K being Cardinal st K <> 0 holds
exp (0,K) = 0 ;

theorem :: CARD_2:27
for K being Cardinal holds
( exp (K,1) = K & exp (1,K) = 1 )
proof
let K be Cardinal; ::_thesis: ( exp (K,1) = K & exp (1,K) = 1 )
thus  exp (K,1) = card K by FUNCT_5:58, ORDINAL3:15
.= K by CARD_1:def_2 ; ::_thesis: exp (1,K) = 1
thus  exp (1,K) = card {(K --> {})} by FUNCT_5:59, ORDINAL3:15
.= 1 by CARD_1:30 ; ::_thesis: verum
end;

theorem :: CARD_2:28
for K, M, N being Cardinal holds exp (K,(M +` N)) = (exp (K,M)) *` (exp (K,N))
proof
let K, M, N be Cardinal; ::_thesis: exp (K,(M +` N)) = (exp (K,M)) *` (exp (K,N))
A1: [:M,{0}:] misses [:N,{1}:] by ZFMISC_1:108;
 [:M,{0}:],M are_equipotent by Th6;
then A2: Funcs ([:M,{0}:],K), Funcs (M,K) are_equipotent by FUNCT_5:60;
 [:N,{1}:],N are_equipotent by Th6;
then A3: Funcs ([:N,{1}:],K), Funcs (N,K) are_equipotent by FUNCT_5:60;
 M +` N,[:M,{0}:] \/ [:N,{1}:] are_equipotent by Th10;
hence  exp (K,(M +` N)) = card (Funcs (([:M,{0}:] \/ [:N,{1}:]),K)) by FUNCT_5:60
.= card [:(Funcs ([:M,{0}:],K)),(Funcs ([:N,{1}:],K)):] by A1, FUNCT_5:62
.= card [:(Funcs (M,K)),(Funcs (N,K)):] by A2, A3, Th8
.= (exp (K,M)) *` (exp (K,N)) by Th7 ;
::_thesis: verum
end;

theorem :: CARD_2:29
for K, M, N being Cardinal holds exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N))
proof
let K, M, N be Cardinal; ::_thesis: exp ((K *` M),N) = (exp (K,N)) *` (exp (M,N))
 ( card (K *` M) = K *` M & card N = card N ) ;
hence  exp ((K *` M),N) = card (Funcs (N,[:K,M:])) by FUNCT_5:61
.= card [:(Funcs (N,K)),(Funcs (N,M)):] by FUNCT_5:64
.= (exp (K,N)) *` (exp (M,N)) by Th7 ;
::_thesis: verum
end;

theorem :: CARD_2:30
for K, M, N being Cardinal holds exp (K,(M *` N)) = exp ((exp (K,M)),N)
proof
let K, M, N be Cardinal; ::_thesis: exp (K,(M *` N)) = exp ((exp (K,M)),N)
A1: Funcs (M,K), card (Funcs (M,K)) are_equipotent by CARD_1:def_2;
 ( [:M,N:],M *` N are_equipotent & [:N,M:],[:M,N:] are_equipotent ) by Lm2, CARD_1:def_2;
then  [:N,M:],M *` N are_equipotent by WELLORD2:15;
hence  exp (K,(M *` N)) = card (Funcs ([:N,M:],K)) by FUNCT_5:60
.= card (Funcs (N,(Funcs (M,K)))) by FUNCT_5:63
.= exp ((exp (K,M)),N) by A1, FUNCT_5:60 ;
::_thesis: verum
end;

theorem :: CARD_2:31
for X being set holds exp (2,(card X)) = card (bool X)
proof
let X be set ; ::_thesis: exp (2,(card X)) = card (bool X)
 ( card (card X) = card X & card 2 = card {{},1} ) by CARD_1:50;
hence  exp (2,(card X)) = card (Funcs (X,{{},1})) by FUNCT_5:61
.= card (bool X) by FUNCT_5:65 ;
::_thesis: verum
end;

theorem :: CARD_2:32
for K being Cardinal holds exp (K,2) = K *` K by CARD_1:50, FUNCT_5:66;

theorem :: CARD_2:33
for K, M being Cardinal holds exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M)
proof
let K, M be Cardinal; ::_thesis: exp ((K +` M),2) = ((K *` K) +` ((2 *` K) *` M)) +` (M *` M)
thus  exp ((K +` M),2) = (K +` M) *` (K +` M) by CARD_1:50, FUNCT_5:66
.= (K *` (K +` M)) +` (M *` (K +` M)) by Th24
.= ((K *` K) +` (K *` M)) +` (M *` (K +` M)) by Th24
.= ((K *` K) +` (K *` M)) +` ((M *` K) +` (M *` M)) by Th24
.= (((K *` K) +` (K *` M)) +` (K *` M)) +` (M *` M) by Th19
.= ((K *` K) +` ((K *` M) +` (K *` M))) +` (M *` M) by Th19
.= ((K *` K) +` (2 *` (K *` M))) +` (M *` M) by Th23
.= ((K *` K) +` ((2 *` K) *` M)) +` (M *` M) by Th22 ; ::_thesis: verum
end;

theorem Th34: :: CARD_2:34
for X, Y being set holds card (X \/ Y) c= (card X) +` (card Y)
proof
let X, Y be set ; ::_thesis: card (X \/ Y) c= (card X) +` (card Y)
consider f being Function such that
A1: ( dom f = H3(X,Y) & ( for x being set st x in H3(X,Y) holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
 X \/ Y c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ Y or x in rng f )
assume  x in X \/ Y ; ::_thesis: x in rng f
then A2: ( x in X or x in Y ) by XBOOLE_0:def_3;
percases ( x in X or not x in X ) ;
suppose x in X ; ::_thesis: x in rng f
then  [x,0] in [:X,{0}:] by ZFMISC_1:106;
then A3: [x,0] in H3(X,Y) by XBOOLE_0:def_3;
 [x,0] `1 = x ;
then  x = f . [x,0] by A1, A3;
hence  x in rng f by A1, A3, FUNCT_1:def_3; ::_thesis: verum
end;
suppose not x in X ; ::_thesis: x in rng f
then  [x,1] in [:Y,{1}:] by A2, ZFMISC_1:106;
then A4: [x,1] in H3(X,Y) by XBOOLE_0:def_3;
 [x,1] `1 = x ;
then  x = f . [x,1] by A1, A4;
hence  x in rng f by A1, A4, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
then  card (X \/ Y) c= card H3(X,Y) by A1, CARD_1:12;
hence  card (X \/ Y) c= (card X) +` (card Y) by Th17; ::_thesis: verum
end;

theorem Th35: :: CARD_2:35
for X, Y being set st X misses Y holds
card (X \/ Y) = (card X) +` (card Y)
proof
let X, Y be set ; ::_thesis: ( X misses Y implies card (X \/ Y) = (card X) +` (card Y) )
assume A1: X misses Y ; ::_thesis: card (X \/ Y) = (card X) +` (card Y)
 ( X,[:X,{0}:] are_equipotent & [:X,{0}:],[:(card X),{0}:] are_equipotent ) by Th6, Th7;
then A2: X,[:(card X),{0}:] are_equipotent by WELLORD2:15;
 ( Y,[:Y,{1}:] are_equipotent & [:Y,{1}:],[:(card Y),{1}:] are_equipotent ) by Th6, Th7;
then A3: Y,[:(card Y),{1}:] are_equipotent by WELLORD2:15;
 [:(card X),{0}:] misses [:(card Y),{1}:] by Lm4;
then  X \/ Y,[:(card X),{0}:] \/ [:(card Y),{1}:] are_equipotent by A1, A2, A3, CARD_1:31;
hence  card (X \/ Y) = card ([:(card X),{0}:] \/ [:(card Y),{1}:]) by CARD_1:5
.= (card X) +` (card Y) by Th10 ;
::_thesis: verum
end;


theorem Th36: :: CARD_2:36
for n, m being Element of NAT holds n + m = n +^ m
proof
let n, m be Element of NAT ; ::_thesis: n + m = n +^ m
defpred S1[ Element of NAT ] means n + $1 = n +^ $1;
A1: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; ::_thesis: S1[m + 1]
thus n + (m + 1) = (n + m) + 1
.= succ (n +^ m) by A2, NAT_1:38
.= n +^ (succ m) by ORDINAL2:28
.= n +^ (m + 1) by NAT_1:38 ; ::_thesis: verum
end;
A3: S1[ 0 ] by ORDINAL2:27;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A1);
hence  n + m = n +^ m ; ::_thesis: verum
end;

theorem Th37: :: CARD_2:37
for n, m being Element of NAT holds n * m = n *^ m
proof
let n, m be Element of NAT ; ::_thesis: n * m = n *^ m
defpred S1[ Element of NAT ] means $1 * m = $1 *^ m;
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus (n + 1) * m = (n * m) + (1 * m)
.= (n *^ m) +^ m by A2, Th36
.= (n *^ m) +^ (1 *^ m) by ORDINAL2:39
.= (n +^ 1) *^ m by ORDINAL3:46
.= (succ n) *^ m by ORDINAL2:31
.= (n + 1) *^ m by NAT_1:38 ; ::_thesis: verum
end;
A3: S1[ 0 ] by ORDINAL2:35;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  n * m = n *^ m ; ::_thesis: verum
end;

theorem Th38: :: CARD_2:38
for n, m being Element of NAT holds card (n + m) = (card n) +` (card m)
proof
let n, m be Element of NAT ; ::_thesis: card (n + m) = (card n) +` (card m)
thus  card (n + m) = card (n +^ m) by Th36
.= (card n) +` (card m) by Th13 ; ::_thesis: verum
end;

theorem Th39: :: CARD_2:39
for n, m being Element of NAT holds card (n * m) = (card n) *` (card m)
proof
let n, m be Element of NAT ; ::_thesis: card (n * m) = (card n) *` (card m)
thus  card (n * m) = card (n *^ m) by Th37
.= (card n) *` (card m) by Th14 ; ::_thesis: verum
end;

theorem Th40: :: CARD_2:40
for X, Y being finite set st X misses Y holds
card (X \/ Y) = (card X) + (card Y)
proof
let X, Y be finite set ; ::_thesis: ( X misses Y implies card (X \/ Y) = (card X) + (card Y) )
assume  X misses Y ; ::_thesis: card (X \/ Y) = (card X) + (card Y)
then  card (card (X \/ Y)) = (card (card X)) +` (card (card Y)) by Th35
.= card ((card X) + (card Y)) by Th38 ;
hence  card (X \/ Y) = (card X) + (card Y) by CARD_1:40; ::_thesis: verum
end;

theorem Th41: :: CARD_2:41
for x being set
for X being finite set st not x in X holds
card (X \/ {x}) = (card X) + 1
proof
let x be set ; ::_thesis: for X being finite set st not x in X holds
card (X \/ {x}) = (card X) + 1
let X be finite set ; ::_thesis: ( not x in X implies card (X \/ {x}) = (card X) + 1 )
A1: card {x} = 1 by CARD_1:30;
assume  not x in X ; ::_thesis: card (X \/ {x}) = (card X) + 1
hence  card (X \/ {x}) = (card X) + 1 by A1, Th40, ZFMISC_1:50; ::_thesis: verum
end;

theorem Th42: :: CARD_2:42
for X being set holds
( card X = 1 iff ex x being set st X = {x} )
proof
let X be set ; ::_thesis: ( card X = 1 iff ex x being set st X = {x} )
 card {0} = 1 by CARD_1:30;
hence  ( card X = 1 implies ex x being set st X = {x} ) by CARD_1:29; ::_thesis: ( ex x being set st X = {x} implies card X = 1 )
given x being set  such that A1: X = {x} ; ::_thesis: card X = 1
thus  card X = 1 by A1, CARD_1:30; ::_thesis: verum
end;

theorem Th43: :: CARD_2:43
for X, Y being finite set holds card (X \/ Y) <= (card X) + (card Y)
proof
let X, Y be finite set ; ::_thesis: card (X \/ Y) <= (card X) + (card Y)
 ( card X = card (card X) & card Y = card (card Y) ) ;
then  (card X) +` (card Y) = card ((card X) + (card Y)) by Th38;
then  ( card (card (X \/ Y)) = card (X \/ Y) & card (X \/ Y) c= card ((card X) + (card Y)) ) by Th34;
hence  card (X \/ Y) <= (card X) + (card Y) by NAT_1:40; ::_thesis: verum
end;

theorem Th44: :: CARD_2:44
for X, Y being finite set st Y c= X holds
card (X \ Y) = (card X) - (card Y)
proof
let X, Y be finite set ; ::_thesis: ( Y c= X implies card (X \ Y) = (card X) - (card Y) )
defpred S1[ set ] means  ex S being finite set st
( S = $1 & card (X \ S) = (card X) - (card S) );
 ( (card X) - 0 = card X & X \ {} = X ) ;
then A1: S1[ {} ] by CARD_1:27;
assume A2: Y c= X ; ::_thesis: card (X \ Y) = (card X) - (card Y)
A3: for X1, Z being set st X1 in Y & Z c= Y & S1[Z] holds
S1[Z \/ {X1}]
proof
let X1, Z be set ; ::_thesis: ( X1 in Y & Z c= Y & S1[Z] implies S1[Z \/ {X1}] )
assume that
A4: X1 in Y and
A5: Z c= Y and
A6: S1[Z] and
A7: not S1[Z \/ {X1}] ; ::_thesis: contradiction
A8: card {X1} = 1 by CARD_1:30;
A9: now__::_thesis:_(_X1_in_Z_implies_S1[Z_\/_{X1}]_)
assume  X1 in Z ; ::_thesis: S1[Z \/ {X1}]
then  {X1} c= Z by ZFMISC_1:31;
then  Z = Z \/ {X1} by XBOOLE_1:12;
hence  S1[Z \/ {X1}] by A6; ::_thesis: verum
end;
then A10: X1 in X \ Z by A2, A4, A7, XBOOLE_0:def_5;
then consider m being Nat such that
A11: card (X \ Z) = m + 1 by NAT_1:6;
reconsider Z1 = Z as finite set by A5;
A12: ( X \ Z, card (X \ Z) are_equipotent & X \ (Z \/ {X1}) = (X \ Z) \ {X1} ) by CARD_1:def_2, XBOOLE_1:41;
 card {X1} = 1 by CARD_1:30;
then A13: (card Z1) + (card {X1}) = card (Z1 \/ {X1}) by A7, A9, Th41;
 m + 1 = succ m by NAT_1:38;
then  ( m in m + 1 & m = (m + 1) \ {m} ) by ORDINAL1:6, ORDINAL1:37;
then  X \ (Z \/ {X1}),m are_equipotent by A10, A11, A12, CARD_1:34;
then  card (X \ (Z \/ {X1})) = (card X) - (card (Z1 \/ {X1})) by A6, A13, A11, A8, CARD_1:def_2;
hence  contradiction by A7; ::_thesis: verum
end;
A14: Y is finite ;
 S1[Y] from FINSET_1:sch_2(A14, A1, A3);
hence  card (X \ Y) = (card X) - (card Y) ; ::_thesis: verum
end;

theorem :: CARD_2:45
for X, Y being finite set holds card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y))
proof
let X, Y be finite set ; ::_thesis: card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y))
 Y \ X = Y \ (X /\ Y) by XBOOLE_1:47;
then A1: card (Y \ X) = (card Y) - (card (X /\ Y)) by Th44, XBOOLE_1:17;
 card (X \/ (Y \ X)) = (card X) + (card (Y \ X)) by Th40, XBOOLE_1:79;
hence  card (X \/ Y) = ((card X) + (card Y)) - (card (X /\ Y)) by A1, XBOOLE_1:39; ::_thesis: verum
end;

theorem :: CARD_2:46
for X, Y being finite set holds card [:X,Y:] = (card X) * (card Y)
proof
let X, Y be finite set ; ::_thesis: card [:X,Y:] = (card X) * (card Y)
card (card [:X,Y:]) = (card (card X)) *` (card (card Y)) by Th7
.= card ((card X) * (card Y)) by Th39 ;
hence  card [:X,Y:] = (card X) * (card Y) by CARD_1:40; ::_thesis: verum
end;

theorem :: CARD_2:47
for f being finite Function holds card (rng f) <= card (dom f) by CARD_1:12, NAT_1:39;

theorem :: CARD_2:48
for X, Y being finite set st X c< Y holds
( card X < card Y & card X in card Y )
proof
let X, Y be finite set ; ::_thesis: ( X c< Y implies ( card X < card Y & card X in card Y ) )
assume A1: X c< Y ; ::_thesis: ( card X < card Y & card X in card Y )
then  X c= Y by XBOOLE_0:def_8;
then A2: Y = X \/ (Y \ X) by XBOOLE_1:45;
then A3: card Y = (card X) + (card (Y \ X)) by Th40, XBOOLE_1:79;
then A4: card X <= card Y by NAT_1:11;
now__::_thesis:_not_card_(Y_\_X)_=_0
assume  card (Y \ X) = 0 ; ::_thesis: contradiction
then  Y \ X = {} ;
hence  contradiction by A1, A2; ::_thesis: verum
end;
then  card X <> card Y by A3;
hence  card X < card Y by A4, XXREAL_0:1; ::_thesis: card X in card Y
hence  card X in card Y by NAT_1:44; ::_thesis: verum
end;

theorem :: CARD_2:49
for X, Y being set st ( card X c= card Y or card X in card Y ) & Y is finite holds
X is finite
proof
let X, Y be set ; ::_thesis: ( ( card X c= card Y or card X in card Y ) & Y is finite implies X is finite )
assume that
A1: ( card X c= card Y or card X in card Y ) and
A2: Y is finite ; ::_thesis: X is finite
 card X c= card Y by A1, ORDINAL1:def_2;
hence  X is finite by A2; ::_thesis: verum
end;


theorem Th50: :: CARD_2:50
for x1, x2 being set holds card {x1,x2} <= 2
proof
let x1, x2 be set ; ::_thesis: card {x1,x2} <= 2
A1: ( {x1,x2} = {x1} \/ {x2} & 1 + 1 = 2 ) by ENUMSET1:1;
 ( card {x1} = 1 & card {x2} = 1 ) by CARD_1:30;
hence  card {x1,x2} <= 2 by A1, Th43; ::_thesis: verum
end;

theorem Th51: :: CARD_2:51
for x1, x2, x3 being set holds card {x1,x2,x3} <= 3
proof
let x1, x2, x3 be set ; ::_thesis: card {x1,x2,x3} <= 3
 card {x2,x3} <= 2 by Th50;
then A1: 1 + (card {x2,x3}) <= 1 + 2 by XREAL_1:7;
 ( card {x1} = 1 & {x1,x2,x3} = {x1} \/ {x2,x3} ) by CARD_1:30, ENUMSET1:2;
then  card {x1,x2,x3} <= 1 + (card {x2,x3}) by Th43;
hence  card {x1,x2,x3} <= 3 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th52: :: CARD_2:52
for x1, x2, x3, x4 being set holds card {x1,x2,x3,x4} <= 4
proof
let x1, x2, x3, x4 be set ; ::_thesis: card {x1,x2,x3,x4} <= 4
 card {x2,x3,x4} <= 3 by Th51;
then A1: 1 + (card {x2,x3,x4}) <= 1 + 3 by XREAL_1:7;
 ( card {x1} = 1 & {x1,x2,x3,x4} = {x1} \/ {x2,x3,x4} ) by CARD_1:30, ENUMSET1:4;
then  card {x1,x2,x3,x4} <= 1 + (card {x2,x3,x4}) by Th43;
hence  card {x1,x2,x3,x4} <= 4 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th53: :: CARD_2:53
for x1, x2, x3, x4, x5 being set holds card {x1,x2,x3,x4,x5} <= 5
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: card {x1,x2,x3,x4,x5} <= 5
 card {x2,x3,x4,x5} <= 4 by Th52;
then A1: 1 + (card {x2,x3,x4,x5}) <= 1 + 4 by XREAL_1:7;
 ( card {x1} = 1 & {x1,x2,x3,x4,x5} = {x1} \/ {x2,x3,x4,x5} ) by CARD_1:30, ENUMSET1:7;
then  card {x1,x2,x3,x4,x5} <= 1 + (card {x2,x3,x4,x5}) by Th43;
hence  card {x1,x2,x3,x4,x5} <= 5 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th54: :: CARD_2:54
for x1, x2, x3, x4, x5, x6 being set holds card {x1,x2,x3,x4,x5,x6} <= 6
proof
let x1, x2, x3, x4, x5, x6 be set ; ::_thesis: card {x1,x2,x3,x4,x5,x6} <= 6
 card {x2,x3,x4,x5,x6} <= 5 by Th53;
then A1: 1 + (card {x2,x3,x4,x5,x6}) <= 1 + 5 by XREAL_1:7;
 ( card {x1} = 1 & {x1,x2,x3,x4,x5,x6} = {x1} \/ {x2,x3,x4,x5,x6} ) by CARD_1:30, ENUMSET1:11;
then  card {x1,x2,x3,x4,x5,x6} <= 1 + (card {x2,x3,x4,x5,x6}) by Th43;
hence  card {x1,x2,x3,x4,x5,x6} <= 6 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th55: :: CARD_2:55
for x1, x2, x3, x4, x5, x6, x7 being set holds card {x1,x2,x3,x4,x5,x6,x7} <= 7
proof
let x1, x2, x3, x4, x5, x6, x7 be set ; ::_thesis: card {x1,x2,x3,x4,x5,x6,x7} <= 7
 card {x2,x3,x4,x5,x6,x7} <= 6 by Th54;
then A1: 1 + (card {x2,x3,x4,x5,x6,x7}) <= 1 + 6 by XREAL_1:7;
 ( card {x1} = 1 & {x1,x2,x3,x4,x5,x6,x7} = {x1} \/ {x2,x3,x4,x5,x6,x7} ) by CARD_1:30, ENUMSET1:16;
then  card {x1,x2,x3,x4,x5,x6,x7} <= 1 + (card {x2,x3,x4,x5,x6,x7}) by Th43;
hence  card {x1,x2,x3,x4,x5,x6,x7} <= 7 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: CARD_2:56
for x1, x2, x3, x4, x5, x6, x7, x8 being set holds card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set ; ::_thesis: card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8
 card {x2,x3,x4,x5,x6,x7,x8} <= 7 by Th55;
then A1: 1 + (card {x2,x3,x4,x5,x6,x7,x8}) <= 1 + 7 by XREAL_1:7;
 ( {x1,x2,x3,x4,x5,x6,x7,x8} = {x1} \/ {x2,x3,x4,x5,x6,x7,x8} & card {x1} = 1 ) by CARD_1:30, ENUMSET1:22;
then  card {x1,x2,x3,x4,x5,x6,x7,x8} <= 1 + (card {x2,x3,x4,x5,x6,x7,x8}) by Th43;
hence  card {x1,x2,x3,x4,x5,x6,x7,x8} <= 8 by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem Th57: :: CARD_2:57
for x1, x2 being set st x1 <> x2 holds
card {x1,x2} = 2
proof
let x1, x2 be set ; ::_thesis: ( x1 <> x2 implies card {x1,x2} = 2 )
A1: ( card {x1} = 1 & card {x2} = 1 ) by CARD_1:30;
A2: ( {x1,x2} = {x1} \/ {x2} & 1 + 1 = 2 ) by ENUMSET1:1;
assume  x1 <> x2 ; ::_thesis: card {x1,x2} = 2
hence  card {x1,x2} = 2 by A1, A2, Th40, ZFMISC_1:11; ::_thesis: verum
end;

theorem Th58: :: CARD_2:58
for x1, x2, x3 being set st x1 <> x2 & x1 <> x3 & x2 <> x3 holds
card {x1,x2,x3} = 3
proof
let x1, x2, x3 be set ; ::_thesis: ( x1 <> x2 & x1 <> x3 & x2 <> x3 implies card {x1,x2,x3} = 3 )
assume  ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) ; ::_thesis: card {x1,x2,x3} = 3
then A1: ( card {x1,x2} = 2 & not x3 in {x1,x2} ) by Th57, TARSKI:def_2;
 {x1,x2,x3} = {x1,x2} \/ {x3} by ENUMSET1:3;
hence  card {x1,x2,x3} = 2 + 1 by A1, Th41
.= 3 ;
::_thesis: verum
end;

theorem Th59: :: CARD_2:59
for x1, x2, x3, x4 being set st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
card {x1,x2,x3,x4} = 4
proof
let x1, x2, x3, x4 be set ; ::_thesis: ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies card {x1,x2,x3,x4} = 4 )
assume  ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 ) ; ::_thesis: card {x1,x2,x3,x4} = 4
then A1: ( card {x1,x2,x3} = 3 & not x4 in {x1,x2,x3} ) by Th58, ENUMSET1:def_1;
 {x1,x2,x3,x4} = {x1,x2,x3} \/ {x4} by ENUMSET1:6;
hence  card {x1,x2,x3,x4} = 3 + 1 by A1, Th41
.= 4 ;
::_thesis: verum
end;

begin

theorem :: CARD_2:60
for X being set st card X = 2 holds
ex x, y being set st
( x <> y & X = {x,y} )
proof
let X be set ; ::_thesis: ( card X = 2 implies ex x, y being set st
( x <> y & X = {x,y} ) )
assume A1: card X = 2 ; ::_thesis: ex x, y being set st
( x <> y & X = {x,y} )
then consider x being set  such that
A2: x in X by CARD_1:27, XBOOLE_0:def_1;
 X is finite by A1;
then reconsider Y = X as finite set ;
 {x} c= X by A2, ZFMISC_1:31;
then  card (X \ {x}) = (card Y) - (card {x}) by Th44
.= 2 - 1 by A1, CARD_1:30 ;
then consider y being set  such that
A3: X \ {x} = {y} by Th42;
take  x ; ::_thesis: ex y being set st
( x <> y & X = {x,y} )
take  y ; ::_thesis: ( x <> y & X = {x,y} )
 x in {x} by TARSKI:def_1;
hence  x <> y by A3, XBOOLE_0:def_5; ::_thesis: X = {x,y}
thus  X c= {x,y} :: according to XBOOLE_0:def_10 ::_thesis: {x,y} c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in X or z in {x,y} )
assume A4: z in X ; ::_thesis: z in {x,y}
percases ( z = x or z <> x ) ;
suppose z = x ; ::_thesis: z in {x,y}
hence  z in {x,y} by TARSKI:def_2; ::_thesis: verum
end;
suppose z <> x ; ::_thesis: z in {x,y}
then  not z in {x} by TARSKI:def_1;
then  z in {y} by A3, A4, XBOOLE_0:def_5;
then  z = y by TARSKI:def_1;
hence  z in {x,y} by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {x,y} or z in X )
assume  z in {x,y} ; ::_thesis: z in X
then A5: ( z = x or z = y ) by TARSKI:def_2;
 y in X \ {x} by A3, TARSKI:def_1;
hence  z in X by A2, A5; ::_thesis: verum
end;

theorem :: CARD_2:61
for f being Function holds card (rng f) c= card (dom f)
proof
let f be Function; ::_thesis: card (rng f) c= card (dom f)
 rng f = f .: (dom f) by RELAT_1:113;
hence  card (rng f) c= card (dom f) by CARD_1:66; ::_thesis: verum
end;

Lm5: now__::_thesis:_for_n_being_Element_of_NAT_st_(_for_Z_being_finite_set_st_card_Z_=_n_&_Z_<>_{}_&_(_for_X,_Y_being_set_st_X_in_Z_&_Y_in_Z_&_not_X_c=_Y_holds_
Y_c=_X_)_holds_
union_Z_in_Z_)_holds_
for_Z_being_finite_set_st_card_Z_=_n_+_1_&_Z_<>_{}_&_(_for_X,_Y_being_set_st_X_in_Z_&_Y_in_Z_&_not_X_c=_Y_holds_
Y_c=_X_)_holds_
union_Z_in_Z
let n be Element of NAT ; ::_thesis: ( ( for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ) implies for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3 )
assume A1: for Z being finite set st card Z = n & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z ; ::_thesis: for Z being finite set st card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union b3 in b3
let Z be finite set ; ::_thesis: ( card Z = n + 1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union b2 in b2 )
assume that
A2: card Z = n + 1 and
A3: Z <> {} and
A4: for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ; ::_thesis: union b2 in b2
set y = the Element of Z;
percases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; ::_thesis: union b2 in b2
then consider x being set  such that
A5: Z = {x} by A2, Th42;
 union Z = x by A5, ZFMISC_1:25;
hence  union Z in Z by A5, TARSKI:def_1; ::_thesis: verum
end;
supposeA6: n <> 0 ; ::_thesis: union b2 in b2
set Y = Z \ { the Element of Z};
reconsider Y = Z \ { the Element of Z} as finite set ;
 { the Element of Z} c= Z by A3, ZFMISC_1:31;
then A7: card Y = (n + 1) - (card { the Element of Z}) by A2, Th44
.= (n + 1) - 1 by CARD_1:30
.= n ;
 for a, b being set st a in Y & b in Y & not a c= b holds
b c= a by A4;
then A8: union Y in Y by A1, A6, A7, CARD_1:27;
then A9: union Y in Z ;
 Z = (Z \ { the Element of Z}) \/ { the Element of Z}
proof
thus  Z c= (Z \ { the Element of Z}) \/ { the Element of Z} :: according to XBOOLE_0:def_10 ::_thesis: (Z \ { the Element of Z}) \/ { the Element of Z} c= Z
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Z or x in (Z \ { the Element of Z}) \/ { the Element of Z} )
assume  x in Z ; ::_thesis: x in (Z \ { the Element of Z}) \/ { the Element of Z}
then  ( x in Z \ { the Element of Z} or x in { the Element of Z} ) by XBOOLE_0:def_5;
hence  x in (Z \ { the Element of Z}) \/ { the Element of Z} by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Z \ { the Element of Z}) \/ { the Element of Z} or x in Z )
assume  x in (Z \ { the Element of Z}) \/ { the Element of Z} ; ::_thesis: x in Z
then A10: ( x in Z \ { the Element of Z} or x in { the Element of Z} ) by XBOOLE_0:def_3;
 { the Element of Z} c= Z by A3, ZFMISC_1:31;
hence  x in Z by A10; ::_thesis: verum
end;
then A11: union Z = (union Y) \/ (union { the Element of Z}) by ZFMISC_1:78
.= (union Y) \/ the Element of Z by ZFMISC_1:25 ;
A12: the Element of Z in Z by A3;
 ( the Element of Z c= union Y or union Y c= the Element of Z ) by A4, A8;
hence  union Z in Z by A9, A12, A11, XBOOLE_1:12; ::_thesis: verum
end;
end;
end;

Lm6:  for Z being finite set st Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z
proof
defpred S1[ Element of NAT ] means  for Z being finite set st card Z = $1 & Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z;
let Z be finite set ; ::_thesis: ( Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union Z in Z )
A1: card Z = card Z ;
A2: S1[ 0 ] ;
A3: for k being Element of NAT st S1[k] holds
S1[k + 1] by Lm5;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A3);
hence  ( Z <> {} & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) implies union Z in Z ) by A1; ::_thesis: verum
end;

theorem :: CARD_2:62
for Z being set st Z <> {} & Z is finite & ( for X, Y being set st X in Z & Y in Z & not X c= Y holds
Y c= X ) holds
union Z in Z by Lm6;

theorem :: CARD_2:63
for x1, x2, x3, x4, x5 being set st x1,x2,x3,x4,x5 are_mutually_different holds
card {x1,x2,x3,x4,x5} = 5
proof
let x1, x2, x3, x4, x5 be set ; ::_thesis: ( x1,x2,x3,x4,x5 are_mutually_different implies card {x1,x2,x3,x4,x5} = 5 )
A1: {x1,x2,x3,x4,x5} = {x1,x2,x3,x4} \/ {x5} by ENUMSET1:10;
assume A2: x1,x2,x3,x4,x5 are_mutually_different ; ::_thesis: card {x1,x2,x3,x4,x5} = 5
then A3: ( x3 <> x5 & x4 <> x5 ) by ZFMISC_1:def_7;
A4: ( x2 <> x4 & x3 <> x4 ) by A2, ZFMISC_1:def_7;
A5: ( x1 <> x4 & x2 <> x3 ) by A2, ZFMISC_1:def_7;
 ( x1 <> x5 & x2 <> x5 ) by A2, ZFMISC_1:def_7;
then A6: not x5 in {x1,x2,x3,x4} by A3, ENUMSET1:def_2;
 ( x1 <> x2 & x1 <> x3 ) by A2, ZFMISC_1:def_7;
then  card {x1,x2,x3,x4} = 4 by A5, A4, Th59;
hence  card {x1,x2,x3,x4,x5} = 4 + 1 by A6, A1, Th41
.= 5 ;
::_thesis: verum
end;

theorem :: CARD_2:64
for M1, M2 being set st card M1 = 0 & card M2 = 0 holds
M1 = M2
proof
let M1, M2 be set ; ::_thesis: ( card M1 = 0 & card M2 = 0 implies M1 = M2 )
assume that
A1: card M1 = {} and
A2: card M2 = {} ; ::_thesis: M1 = M2
 M1 = {} by A1;
hence  M1 = M2 by A2; ::_thesis: verum
end;

registration
let x, y be set ;
cluster[x,y] ->  non natural ;
coherence
 not [x,y] is natural
proof
assume  [x,y] is natural ; ::_thesis: contradiction
then reconsider n = [x,y] as Nat ;
 card n <= 2 by Th50;
then A1: n <= 2 by CARD_1:def_2;
percases ( n = 0 or n = 1 or n = 2 ) by A1, NAT_1:26;
suppose n = 0 ; ::_thesis: contradiction
hence  contradiction ; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: contradiction
hence  contradiction by CARD_1:49, ZFMISC_1:4; ::_thesis: verum
end;
suppose n = 2 ; ::_thesis: contradiction
hence  contradiction by CARD_1:50, ZFMISC_1:6; ::_thesis: verum
end;
end;
end;
end;

begin


theorem :: CARD_2:65
for M, N being Cardinal holds Sum (M --> N) = M *` N
proof
let M, N be Cardinal; ::_thesis: Sum (M --> N) = M *` N
thus  Sum (M --> N) = card [:N,M:] by CARD_3:25
.= M *` N by Lm2 ; ::_thesis: verum
end;

theorem :: CARD_2:66
for N, M being Cardinal holds Product (N --> M) = exp (M,N) by CARD_3:11;

scheme :: CARD_2:sch 1
FinRegularity{ F1() ->  finite set , P1[ set , set ] } :
 ex x being set st
( x in F1() & ( for y being set st y in F1() & y <> x holds
not P1[y,x] ) )
provided
A1: F1() <> {} and
A2: for x, y being set st P1[x,y] & P1[y,x] holds
x = y and
A3: for x, y, z being set st P1[x,y] & P1[y,z] holds
P1[x,z]
proof
defpred S1[ Nat] means  for X being finite set st card X = $1 & X <> {} holds
ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) );
A4: S1[ 0 ] ;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A6: for X being finite set st card X = n & X <> {} holds
ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) ; ::_thesis: S1[n + 1]
let X be finite set ; ::_thesis: ( card X = n + 1 & X <> {} implies ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) )
assume that
A7: card X = n + 1 and
A8: X <> {} ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
set x = the Element of X;
A9: now__::_thesis:_(_X_\_{_the_Element_of_X}_=_{}_implies_ex_x_being_set_st_
(_x_in_X_&_(_for_y_being_set_st_y_in_X_&_y_<>_x_holds_
not_P1[y,x]_)_)_)
assume  X \ { the Element of X} = {} ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
then A10: X c= { the Element of X} by XBOOLE_1:37;
thus  ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) ::_thesis: verum
proof
take  the Element of X ; ::_thesis: ( the Element of X in X & ( for y being set st y in X & y <> the Element of X holds
not P1[y, the Element of X] ) )
thus  the Element of X in X by A8; ::_thesis: for y being set st y in X & y <> the Element of X holds
not P1[y, the Element of X]
thus  for y being set st y in X & y <> the Element of X holds
not P1[y, the Element of X] by A10, TARSKI:def_1; ::_thesis: verum
end;
end;
now__::_thesis:_(_X_\_{_the_Element_of_X}_<>_{}_implies_ex_x_being_set_st_
(_x_in_X_&_(_for_y_being_set_st_y_in_X_&_y_<>_x_holds_
not_P1[y,x]_)_)_)
assume A11: X \ { the Element of X} <> {} ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
 { the Element of X} c= X by A8, ZFMISC_1:31;
then A12: card (X \ { the Element of X}) = (n + 1) - (card { the Element of X}) by A7, Th44;
 card { the Element of X} = 1 by CARD_1:30;
then consider y being set  such that
A13: y in X \ { the Element of X} and
A14: for z being set st z in X \ { the Element of X} & z <> y holds
not P1[z,y] by A6, A11, A12;
A15: now__::_thesis:_(_P1[_the_Element_of_X,y]_implies_ex_x_being_set_st_
(_x_in_X_&_(_for_y_being_set_st_y_in_X_&_y_<>_x_holds_
not_P1[y,x]_)_)_)
assume A16: P1[ the Element of X,y] ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
thus  ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) ::_thesis: verum
proof
take  the Element of X ; ::_thesis: ( the Element of X in X & ( for y being set st y in X & y <> the Element of X holds
not P1[y, the Element of X] ) )
thus  the Element of X in X by A8; ::_thesis: for y being set st y in X & y <> the Element of X holds
not P1[y, the Element of X]
let z be set ; ::_thesis: ( z in X & z <> the Element of X implies not P1[z, the Element of X] )
assume that
A17: z in X and
A18: z <> the Element of X and
A19: P1[z, the Element of X] ; ::_thesis: contradiction
 not z in { the Element of X} by A18, TARSKI:def_1;
then A20: z in X \ { the Element of X} by A17, XBOOLE_0:def_5;
A21: not y in { the Element of X} by A13, XBOOLE_0:def_5;
A22: z = y by A3, A14, A16, A19, A20;
 y <> the Element of X by A21, TARSKI:def_1;
hence  contradiction by A2, A16, A19, A22; ::_thesis: verum
end;
end;
now__::_thesis:_(_P1[_the_Element_of_X,y]_implies_ex_x_being_set_st_
(_x_in_X_&_(_for_y_being_set_st_y_in_X_&_y_<>_x_holds_
not_P1[y,x]_)_)_)
assume A23: P1[ the Element of X,y] ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) )
thus  ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) ::_thesis: verum
proof
take  y ; ::_thesis: ( y in X & ( for y being set st y in X & y <> y holds
not P1[y,y] ) )
thus  y in X by A13; ::_thesis: for y being set st y in X & y <> y holds
not P1[y,y]
let z be set ; ::_thesis: ( z in X & z <> y implies not P1[z,y] )
assume that
A24: z in X and
A25: z <> y ; ::_thesis: P1[z,y]
 ( z in { the Element of X} or not z in { the Element of X} ) ;
then  ( z = the Element of X or z in X \ { the Element of X} ) by A24, TARSKI:def_1, XBOOLE_0:def_5;
hence  P1[z,y] by A14, A23, A25; ::_thesis: verum
end;
end;
hence  ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) by A15; ::_thesis: verum
end;
hence  ex x being set st
( x in X & ( for y being set st y in X & y <> x holds
not P1[y,x] ) ) by A9; ::_thesis: verum
end;
A26: for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5);
 card F1() = card F1() ;
hence  ex x being set st
( x in F1() & ( for y being set st y in F1() & y <> x holds
not P1[y,x] ) ) by A1, A26; ::_thesis: verum
end;

scheme :: CARD_2:sch 2
MaxFinSetElem{ F1() ->  finite set , P1[ set , set ] } :
 ex x being set st
( x in F1() & ( for y being set st y in F1() holds
P1[x,y] ) )
provided
A1: F1() <> {} and
A2: for x, y being set holds
( P1[x,y] or P1[y,x] ) and
A3: for x, y, z being set st P1[x,y] & P1[y,z] holds
P1[x,z]
proof
defpred S1[ Nat] means  for X being finite set st card X = $1 & X <> {} holds
ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) );
A4: S1[ 0 ] ;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A6: for X being finite set st card X = n & X <> {} holds
ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) ; ::_thesis: S1[n + 1]
let X be finite set ; ::_thesis: ( card X = n + 1 & X <> {} implies ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) )
assume that
A7: card X = n + 1 and
A8: X <> {} ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) )
set x = the Element of X;
A9: now__::_thesis:_(_X_\_{_the_Element_of_X}_=_{}_implies_ex_x_being_set_st_
(_x_in_X_&_(_for_y_being_set_st_y_in_X_holds_
P1[x,y]_)_)_)
assume  X \ { the Element of X} = {} ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) )
then A10: X c= { the Element of X} by XBOOLE_1:37;
thus  ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) ::_thesis: verum
proof
take  the Element of X ; ::_thesis: ( the Element of X in X & ( for y being set st y in X holds
P1[ the Element of X,y] ) )
thus  the Element of X in X by A8; ::_thesis: for y being set st y in X holds
P1[ the Element of X,y]
let y be set ; ::_thesis: ( y in X implies P1[ the Element of X,y] )
assume  y in X ; ::_thesis: P1[ the Element of X,y]
then  y = the Element of X by A10, TARSKI:def_1;
hence  P1[ the Element of X,y] by A2; ::_thesis: verum
end;
end;
now__::_thesis:_(_X_\_{_the_Element_of_X}_<>_{}_implies_ex_x_being_set_st_
(_x_in_X_&_(_for_y_being_set_st_y_in_X_holds_
P1[x,y]_)_)_)
assume A11: X \ { the Element of X} <> {} ; ::_thesis: ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) )
 { the Element of X} c= X by A8, ZFMISC_1:31;
then A12: card (X \ { the Element of X}) = (n + 1) - (card { the Element of X}) by A7, Th44;
 card { the Element of X} = 1 by CARD_1:30;
then consider y being set  such that
A13: y in X \ { the Element of X} and
A14: for z being set st z in X \ { the Element of X} holds
P1[y,z] by A6, A11, A12;
A15: ( P1[ the Element of X,y] or P1[y, the Element of X] ) by A2;
A16: P1[ the Element of X, the Element of X] by A2;
 P1[y,y] by A2;
then consider z being set  such that
A17: ( z = the Element of X or z = y ) and
A18: P1[z, the Element of X] and
A19: P1[z,y] by A15, A16;
thus  ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) ::_thesis: verum
proof
take  z ; ::_thesis: ( z in X & ( for y being set st y in X holds
P1[z,y] ) )
thus  z in X by A13, A17; ::_thesis: for y being set st y in X holds
P1[z,y]
let u be set ; ::_thesis: ( u in X implies P1[z,u] )
A20: ( u in { the Element of X} or not u in { the Element of X} ) ;
assume  u in X ; ::_thesis: P1[z,u]
then  ( u = the Element of X or u in X \ { the Element of X} ) by A20, TARSKI:def_1, XBOOLE_0:def_5;
then  ( P1[z,u] or P1[y,u] ) by A14, A18;
hence  P1[z,u] by A3, A19; ::_thesis: verum
end;
end;
hence  ex x being set st
( x in X & ( for y being set st y in X holds
P1[x,y] ) ) by A9; ::_thesis: verum
end;
A21: for n being Nat holds S1[n] from NAT_1:sch_2(A4, A5);
 card F1() = card F1() ;
hence  ex x being set st
( x in F1() & ( for y being set st y in F1() holds
P1[x,y] ) ) by A1, A21; ::_thesis: verum
end;

Lm7:  for n being Nat st Rank n is finite holds
Rank (n + 1) is finite
proof
let n be Nat; ::_thesis: ( Rank n is finite implies Rank (n + 1) is finite )
 n + 1 = succ n by NAT_1:38;
then  Rank (n + 1) = bool (Rank n) by CLASSES1:30;
hence  ( Rank n is finite implies Rank (n + 1) is finite ) ; ::_thesis: verum
end;

Lm8:  1 = card 1
by CARD_1:def_2;

Lm9:  2 = card 2
by CARD_1:def_2;

theorem :: CARD_2:67
for n being Nat holds Rank n is finite
proof
let n be Nat; ::_thesis: Rank n is finite
defpred S1[ Nat] means  Rank $1 is finite ;
A1: S1[ 0 ] by CLASSES1:29;
A2: for n being Nat st S1[n] holds
S1[n + 1] by Lm7;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  Rank n is finite ; ::_thesis: verum
end;

theorem :: CARD_2:68
for M being Cardinal holds
( 0 in M iff 1 c= M )
proof
let M be Cardinal; ::_thesis: ( 0 in M iff 1 c= M )
 0 + 1 = 1 ;
then  nextcard (card 0) = card 1 by NAT_1:42;
hence  ( 0 in M iff 1 c= M ) by Lm8, CARD_3:90; ::_thesis: verum
end;

theorem :: CARD_2:69
for M being Cardinal holds
( 1 in M iff 2 c= M )
proof
let M be Cardinal; ::_thesis: ( 1 in M iff 2 c= M )
 1 + 1 = 2 ;
then  nextcard (card 1) = card 2 by NAT_1:42;
hence  ( 1 in M iff 2 c= M ) by Lm8, Lm9, CARD_3:90; ::_thesis: verum
end;


theorem Th70: :: CARD_2:70
for A being Ordinal holds
( A is limit_ordinal iff for B being Ordinal
for n being Nat st B in A holds
B +^ n in A )
proof
let A be Ordinal; ::_thesis: ( A is limit_ordinal iff for B being Ordinal
for n being Nat st B in A holds
B +^ n in A )
thus  ( A is limit_ordinal implies for B being Ordinal
for n being Nat st B in A holds
B +^ n in A ) ::_thesis: ( ( for B being Ordinal
for n being Nat st B in A holds
B +^ n in A ) implies A is limit_ordinal )
proof
assume A1: A is limit_ordinal ; ::_thesis: for B being Ordinal
for n being Nat st B in A holds
B +^ n in A
let B be Ordinal; ::_thesis: for n being Nat st B in A holds
B +^ n in A
let n be Nat; ::_thesis: ( B in A implies B +^ n in A )
defpred S1[ Nat] means B +^ $1 in A;
assume  B in A ; ::_thesis: B +^ n in A
then A2: S1[ 0 ] by ORDINAL2:27;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
 k + 1 = succ k by NAT_1:38;
then  B +^ (k + 1) = succ (B +^ k) by ORDINAL2:28;
hence  ( S1[k] implies S1[k + 1] ) by A1, ORDINAL1:28; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A2, A3);
hence  B +^ n in A ; ::_thesis: verum
end;
assume A4: for B being Ordinal
for n being Nat st B in A holds
B +^ n in A ; ::_thesis: A is limit_ordinal
now__::_thesis:_for_B_being_Ordinal_st_B_in_A_holds_
succ_B_in_A
let B be Ordinal; ::_thesis: ( B in A implies succ B in A )
assume  B in A ; ::_thesis: succ B in A
then  B +^ 1 in A by A4;
hence  succ B in A by ORDINAL2:31; ::_thesis: verum
end;
hence  A is limit_ordinal by ORDINAL1:28; ::_thesis: verum
end;

theorem Th71: :: CARD_2:71
for A being Ordinal
for n being Nat holds
( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )
proof
let A be Ordinal; ::_thesis: for n being Nat holds
( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )
let n be Nat; ::_thesis: ( A +^ (succ n) = (succ A) +^ n & A +^ (n + 1) = (succ A) +^ n )
defpred S1[ Nat] means A +^ (succ $1) = (succ A) +^ $1;
A +^ (succ 0) = succ A by ORDINAL2:31
.= (succ A) +^ 0 by ORDINAL2:27 ;
then A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
A4: k + 1 = succ k by NAT_1:38;
hence A +^ (succ (k + 1)) = succ ((succ A) +^ k) by A3, ORDINAL2:28
.= ((succ A) +^ k) +^ 1 by ORDINAL2:31
.= (succ A) +^ (k +^ 1) by ORDINAL3:30
.= (succ A) +^ (k + 1) by A4, ORDINAL2:31 ;
::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  A +^ (succ n) = (succ A) +^ n ; ::_thesis: A +^ (n + 1) = (succ A) +^ n
hence  A +^ (n + 1) = (succ A) +^ n by NAT_1:38; ::_thesis: verum
end;

theorem Th72: :: CARD_2:72
for A being Ordinal ex n being Nat st A *^ (succ 1) = A +^ n
proof
let A be Ordinal; ::_thesis: ex n being Nat st A *^ (succ 1) = A +^ n
defpred S1[ Ordinal] means  ex n being Nat st $1 *^ 2 = $1 +^ n;
 {} +^ {} = {} by ORDINAL2:27;
then A1: S1[ 0 ] by ORDINAL2:35;
A2: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
given n being Nat such that A3: A *^ 2 = A +^ n ; ::_thesis: S1[ succ A]
take  n + 1 ; ::_thesis: (succ A) *^ 2 = (succ A) +^ (n + 1)
(succ A) *^ 2 = (A *^ 2) +^ 2 by ORDINAL2:36
.= succ ((A *^ (succ 1)) +^ 1) by ORDINAL2:28
.= succ (succ (A +^ n)) by A3, ORDINAL2:31
.= succ (A +^ (succ n)) by ORDINAL2:28
.= succ (A +^ (n + 1)) by NAT_1:38
.= A +^ (succ (n + 1)) by ORDINAL2:28 ;
hence  (succ A) *^ 2 = (succ A) +^ (n + 1) by Th71; ::_thesis: verum
end;
A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A5: A <> {} and
A6: A is limit_ordinal and
A7: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
take  0 ; ::_thesis: A *^ 2 = A +^ 0
deffunc H5( Ordinal) ->  set = $1 *^ 2;
consider phi being Ordinal-Sequence such that
A8: dom phi = A and
A9: for B being Ordinal st B in A holds
phi . B = H5(B) from ORDINAL2:sch_3();
A10: A *^ 2 = union (sup phi) by A5, A6, A8, A9, ORDINAL2:37
.= union (sup (rng phi)) by ORDINAL2:26 ;
thus  A *^ 2 c= A +^ 0 :: according to XBOOLE_0:def_10 ::_thesis: A +^ 0 c= A *^ 2
proof
let B be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not B in A *^ 2 or B in A +^ 0 )
assume  B in A *^ 2 ; ::_thesis: B in A +^ 0
then consider X being set  such that
A11: B in X and
A12: X in sup (rng phi) by A10, TARSKI:def_4;
reconsider X = X as Ordinal by A12;
consider C being Ordinal such that
A13: C in rng phi and
A14: X c= C by A12, ORDINAL2:21;
consider x being set  such that
A15: x in dom phi and
A16: C = phi . x by A13, FUNCT_1:def_3;
reconsider x = x as Ordinal by A15;
A17: ex n being Nat st x *^ 2 = x +^ n by A7, A8, A15;
 C = x *^ 2 by A8, A9, A15, A16;
then A18: C in A by A6, A8, A15, A17, Th70;
 A +^ {} = A by ORDINAL2:27;
hence  B in A +^ 0 by A11, A14, A18, ORDINAL1:10; ::_thesis: verum
end;
A19: 1 in succ 1 by ORDINAL1:6;
A20: A +^ 0 = A by ORDINAL2:27;
A21: A = A *^ 1 by ORDINAL2:39;
 1 c= 2 by A19, ORDINAL1:def_2;
hence  A +^ 0 c= A *^ 2 by A20, A21, ORDINAL2:42; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A1, A2, A4);
hence  ex n being Nat st A *^ (succ 1) = A +^ n ; ::_thesis: verum
end;

theorem Th73: :: CARD_2:73
for A being Ordinal st A is limit_ordinal holds
A *^ (succ 1) = A
proof
let A be Ordinal; ::_thesis: ( A is limit_ordinal implies A *^ (succ 1) = A )
consider n being Nat such that
A1: A *^ 2 = A +^ n by Th72;
assume  A is limit_ordinal ; ::_thesis: A *^ (succ 1) = A
then A2: A +^ n is limit_ordinal by A1, ORDINAL3:40;
now__::_thesis:_not_n_<>_0
assume  n <> 0 ; ::_thesis: contradiction
then consider k being Nat such that
A3: n = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
 n = succ k by A3, NAT_1:38;
then  A +^ n = succ (A +^ k) by ORDINAL2:28;
hence  contradiction by A2, ORDINAL1:29; ::_thesis: verum
end;
hence  A *^ (succ 1) = A by A1, ORDINAL2:27; ::_thesis: verum
end;

Lm10:  omega is limit_ordinal
by ORDINAL1:def_11;

theorem Th74: :: CARD_2:74
for A being Ordinal st omega c= A holds
1 +^ A = A
proof
let A be Ordinal; ::_thesis: ( omega c= A implies 1 +^ A = A )
deffunc H5( Ordinal) ->  set = 1 +^ $1;
consider phi being Ordinal-Sequence such that
A1: ( dom phi = omega & ( for B being Ordinal st B in omega holds
phi . B = H5(B) ) ) from ORDINAL2:sch_3();
A2: 1 +^ omega = sup phi by A1, Lm10, ORDINAL2:29
.= sup (rng phi) by ORDINAL2:26 ;
A3: 1 +^ omega c= omega
proof
let B be Ordinal; :: according to ORDINAL1:def_5 ::_thesis: ( not B in 1 +^ omega or B in omega )
assume  B in 1 +^ omega ; ::_thesis: B in omega
then consider C being Ordinal such that
A4: C in rng phi and
A5: B c= C by A2, ORDINAL2:21;
consider x being set  such that
A6: x in dom phi and
A7: C = phi . x by A4, FUNCT_1:def_3;
reconsider x = x as Ordinal by A6;
reconsider x9 = x as Cardinal by A1, A6;
reconsider x = x as finite Ordinal by A1, A6;
A8: C = 1 +^ x by A1, A6, A7;
 succ x in omega by A1, A6, Lm10, ORDINAL1:28;
then  C in omega by A8, ORDINAL2:31;
hence  B in omega by A5, ORDINAL1:12; ::_thesis: verum
end;
assume  omega c= A ; ::_thesis: 1 +^ A = A
then A9: ex B being Ordinal st A = omega +^ B by ORDINAL3:27;
 omega c= 1 +^ omega by ORDINAL3:24;
then  omega = 1 +^ omega by A3, XBOOLE_0:def_10;
hence  1 +^ A = A by A9, ORDINAL3:30; ::_thesis: verum
end;

registration
cluster infinite cardinal  ->  limit_ordinal for set ;
coherence
 for b1 being Cardinal st b1 is infinite holds
b1 is limit_ordinal
proof
let M be Cardinal; ::_thesis: ( M is infinite implies M is limit_ordinal )
assume  M is infinite ; ::_thesis: M is limit_ordinal
then A1: not M in omega ;
assume  not M is limit_ordinal ; ::_thesis: contradiction
then consider A being Ordinal such that
A2: M = succ A by ORDINAL1:29;
 ( ( omega <> M & omega c= M ) iff omega c< M ) by XBOOLE_0:def_8;
then  ( omega = succ A or omega in succ A ) by A1, A2, CARD_1:4, ORDINAL1:11;
then A3: omega c= A by Lm10, ORDINAL1:22, ORDINAL1:29;
card (A +^ 1) = (card 1) +` (card A) by Th13
.= card (1 +^ A) by Th13
.= card A by A3, Th74 ;
then  card (succ A) = card A by ORDINAL2:31;
then A4: A, succ A are_equipotent by CARD_1:5;
A5: not succ A c= A by ORDINAL1:5, ORDINAL1:6;
 ex B being Ordinal st
( succ A = B & ( for A being Ordinal st A,B are_equipotent holds
B c= A ) ) by A2, CARD_1:def_1;
hence  contradiction by A4, A5; ::_thesis: verum
end;
end;

theorem Th75: :: CARD_2:75
for M being Cardinal st not M is finite holds
M +` M = M
proof
let M be Cardinal; ::_thesis: ( not M is finite implies M +` M = M )
assume  not M is finite ; ::_thesis: M +` M = M
then  M *^ (succ 1) = M by Th73;
then  card M = (card 2) *` (card M) by Th14
.= card ((succ 1) *^ M) by Th14
.= card ((1 *^ M) +^ M) by ORDINAL2:36
.= M +` M by ORDINAL2:39 ;
hence  M +` M = M by CARD_1:def_2; ::_thesis: verum
end;

theorem Th76: :: CARD_2:76
for M, N being Cardinal st not M is finite & ( N c= M or N in M ) holds
( M +` N = M & N +` M = M )
proof
let M, N be Cardinal; ::_thesis: ( not M is finite & ( N c= M or N in M ) implies ( M +` N = M & N +` M = M ) )
assume that
A1: not M is finite and
A2: ( N c= M or N in M ) ; ::_thesis: ( M +` N = M & N +` M = M )
A3: M +` M = M by A1, Th75;
 N c= M by A2, CARD_1:3;
then A4: M +^ N c= M +^ M by ORDINAL2:33;
A5: M c= M +^ N by ORDINAL3:24;
A6: card M = M by A3;
A7: M +` N c= M by A3, A4, CARD_1:11;
 M c= M +` N by A5, A6, CARD_1:11;
hence  ( M +` N = M & N +` M = M ) by A7, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CARD_2:77
for X, Y being set st not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
proof
let X, Y be set ; ::_thesis: ( not X is finite & ( X,Y are_equipotent or Y,X are_equipotent ) implies ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) )
assume that
A1: not X is finite and
A2: ( X,Y are_equipotent or Y,X are_equipotent ) ; ::_thesis: ( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
A3: card X = card Y by A2, CARD_1:5;
A4: card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
A5: card (X \/ Y) c= (card X) +` (card Y) by Th34;
 (card X) +` (card Y) = card X by A1, A3, Th75;
then  card X = card (X \/ Y) by A4, A5, XBOOLE_0:def_10;
hence  ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) by CARD_1:5; ::_thesis: verum
end;

theorem :: CARD_2:78
for X, Y being set st not X is finite & Y is finite holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
proof
let X, Y be set ; ::_thesis: ( not X is finite & Y is finite implies ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) )
assume that
A1: not X is finite and
A2: Y is finite ; ::_thesis: ( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
 card Y in card X by A1, A2, CARD_3:86;
then A3: (card X) +` (card Y) = card X by A1, Th76;
A4: card (X \/ Y) c= (card X) +` (card Y) by Th34;
 card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
then  card X = card (X \/ Y) by A3, A4, XBOOLE_0:def_10;
hence  ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) by CARD_1:5; ::_thesis: verum
end;

theorem :: CARD_2:79
for X, Y being set st not X is finite & ( card Y in card X or card Y c= card X ) holds
( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
proof
let X, Y be set ; ::_thesis: ( not X is finite & ( card Y in card X or card Y c= card X ) implies ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) )
assume that
A1: not X is finite and
A2: ( card Y in card X or card Y c= card X ) ; ::_thesis: ( X \/ Y,X are_equipotent & card (X \/ Y) = card X )
A3: (card X) +` (card Y) = card X by A1, A2, Th76;
A4: card (X \/ Y) c= (card X) +` (card Y) by Th34;
 card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
then  card X = card (X \/ Y) by A3, A4, XBOOLE_0:def_10;
hence  ( X \/ Y,X are_equipotent & card (X \/ Y) = card X ) by CARD_1:5; ::_thesis: verum
end;

theorem :: CARD_2:80
for M, N being finite Cardinal holds M +` N is finite
proof
let M, N be finite Cardinal; ::_thesis: M +` N is finite
A1: card M = M by CARD_1:def_2;
 card N = N by CARD_1:def_2;
then  M +` N = card ((card M) + (card N)) by A1, Th38;
hence  M +` N is finite ; ::_thesis: verum
end;

theorem :: CARD_2:81
for M, N being Cardinal st not M is finite holds
( not M +` N is finite & not N +` M is finite )
proof
let M, N be Cardinal; ::_thesis: ( not M is finite implies ( not M +` N is finite & not N +` M is finite ) )
assume A1: not M is finite ; ::_thesis: ( not M +` N is finite & not N +` M is finite )
 ( M c= N or N c= M ) ;
then  ( ( M c= N & not N is finite ) or ( M +` N = M & N +` M = M ) ) by A1, Th76;
hence  ( not M +` N is finite & not N +` M is finite ) by A1, Th76; ::_thesis: verum
end;

theorem :: CARD_2:82
for M, N being finite Cardinal holds M *` N is finite ;

theorem Th83: :: CARD_2:83
for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds
( K +` M c= L +` N & M +` K c= L +` N )
proof
let K, L, M, N be Cardinal; ::_thesis: ( ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) implies ( K +` M c= L +` N & M +` K c= L +` N ) )
assume A1: ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) ; ::_thesis: ( K +` M c= L +` N & M +` K c= L +` N )
A2: K c= L by A1, CARD_1:3;
A3: M c= N by A1, CARD_1:3;
A4: K +` M = card (K +^ M) ;
A5: K +^ M c= L +^ N by A2, A3, ORDINAL3:18;
hence  K +` M c= L +` N by CARD_1:11; ::_thesis: M +` K c= L +` N
thus  M +` K c= L +` N by A4, A5, CARD_1:11; ::_thesis: verum
end;

theorem :: CARD_2:84
for M, N, K being Cardinal st ( M in N or M c= N ) holds
( K +` M c= K +` N & K +` M c= N +` K & M +` K c= K +` N & M +` K c= N +` K ) by Th83;

theorem Th85: :: CARD_2:85
for X, Y being set st X is countable & Y is countable holds
X \/ Y is countable
proof
let X, Y be set ; ::_thesis: ( X is countable & Y is countable implies X \/ Y is countable )
assume that
A1: card X c= omega and
A2: card Y c= omega ; :: according to CARD_3:def_14 ::_thesis: X \/ Y is countable
A3: card (X \/ Y) c= (card X) +` (card Y) by Th34;
A4: omega +` omega = omega by Th75;
 (card X) +` (card Y) c= omega +` omega by A1, A2, Th83;
hence  card (X \/ Y) c= omega by A3, A4, XBOOLE_1:1; :: according to CARD_3:def_14 ::_thesis: verum
end;

theorem Th86: :: CARD_2:86
for M, N being Cardinal
for f being Function st card (dom f) c= M & ( for x being set st x in dom f holds
card (f . x) c= N ) holds
card (Union f) c= M *` N
proof
let M, N be Cardinal; ::_thesis: for f being Function st card (dom f) c= M & ( for x being set st x in dom f holds
card (f . x) c= N ) holds
card (Union f) c= M *` N
let f be Function; ::_thesis: ( card (dom f) c= M & ( for x being set st x in dom f holds
card (f . x) c= N ) implies card (Union f) c= M *` N )
assume that
A1: card (dom f) c= M and
A2: for x being set st x in dom f holds
card (f . x) c= N ; ::_thesis: card (Union f) c= M *` N
A3: card (Union f) c= Sum (Card f) by CARD_3:39;
A4: dom (Card f) = dom f by CARD_3:def_2;
A5: dom ((dom f) --> N) = dom f by FUNCOP_1:13;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Card_f)_holds_
(Card_f)_._x_c=_((dom_f)_-->_N)_._x
let x be set ; ::_thesis: ( x in dom (Card f) implies (Card f) . x c= ((dom f) --> N) . x )
assume A6: x in dom (Card f) ; ::_thesis: (Card f) . x c= ((dom f) --> N) . x
then A7: (Card f) . x = card (f . x) by A4, CARD_3:def_2;
 ((dom f) --> N) . x = N by A4, A6, FUNCOP_1:7;
hence  (Card f) . x c= ((dom f) --> N) . x by A2, A4, A6, A7; ::_thesis: verum
end;
then  Sum (Card f) c= Sum ((dom f) --> N) by A4, A5, CARD_3:30;
then A8: card (Union f) c= Sum ((dom f) --> N) by A3, XBOOLE_1:1;
A9: [:(card (dom f)),N:] c= [:M,N:] by A1, ZFMISC_1:95;
Sum ((dom f) --> N) = card [:N,(dom f):] by CARD_3:25
.= card [:N,(card (dom f)):] by Th7
.= card [:(card (dom f)),N:] by Th4 ;
then A10: Sum ((dom f) --> N) c= card [:M,N:] by A9, CARD_1:11;
thus  card (Union f) c= M *` N by A8, A10, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: CARD_2:87
for M, N being Cardinal
for X being set st card X c= M & ( for Y being set st Y in X holds
card Y c= N ) holds
card (union X) c= M *` N
proof
let M, N be Cardinal; ::_thesis: for X being set st card X c= M & ( for Y being set st Y in X holds
card Y c= N ) holds
card (union X) c= M *` N
let X be set ; ::_thesis: ( card X c= M & ( for Y being set st Y in X holds
card Y c= N ) implies card (union X) c= M *` N )
assume that
A1: card X c= M and
A2: for Y being set st Y in X holds
card Y c= N ; ::_thesis: card (union X) c= M *` N
now__::_thesis:_for_x_being_set_st_x_in_dom_(id_X)_holds_
card_((id_X)_._x)_c=_N
let x be set ; ::_thesis: ( x in dom (id X) implies card ((id X) . x) c= N )
assume  x in dom (id X) ; ::_thesis: card ((id X) . x) c= N
then  (id X) . x in X by FUNCT_1:18;
hence  card ((id X) . x) c= N by A2; ::_thesis: verum
end;
then  card (Union (id X)) c= M *` N by A1, Th86;
hence  card (union X) c= M *` N ; ::_thesis: verum
end;

theorem Th88: :: CARD_2:88
for f being Function st dom f is finite & ( for x being set st x in dom f holds
f . x is finite ) holds
Union f is finite
proof
let f be Function; ::_thesis: ( dom f is finite & ( for x being set st x in dom f holds
f . x is finite ) implies Union f is finite )
assume that
A1: dom f is finite and
A2: for x being set st x in dom f holds
f . x is finite ; ::_thesis: Union f is finite
reconsider df = dom f as finite set by A1;
now__::_thesis:_(_dom_f_<>_{}_implies_Union_f_is_finite_)
assume  dom f <> {} ; ::_thesis: Union f is finite
then A3: df <> {} ;
defpred S1[ set , set ] means  card (f . $2) c= card (f . $1);
A4: for x, y being set holds
( S1[x,y] or S1[y,x] ) ;
A5: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z] by XBOOLE_1:1;
consider x being set  such that
A6: ( x in df & ( for y being set st y in df holds
S1[x,y] ) ) from CARD_2:sch_2(A3, A4, A5);
reconsider fx = f . x as finite set by A2, A6;
A7: card (Union f) c= (card (card df)) *` (card (f . x)) by A6, Th86;
 card (f . x) = card (card fx) ;
then  card (Union f) c= card ((card df) * (card fx)) by A7, Th39;
hence  Union f is finite ; ::_thesis: verum
end;
hence  Union f is finite by RELAT_1:42, ZFMISC_1:2; ::_thesis: verum
end;

theorem :: CARD_2:89
for n being Nat holds
( omega *` (card n) c= omega & (card n) *` omega c= omega )
proof
let n be Nat; ::_thesis: ( omega *` (card n) c= omega & (card n) *` omega c= omega )
defpred S1[ Nat] means omega *` (card $1) c= omega ;
A1: S1[ 0 ] ;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
card (k + 1) = k + 1 by CARD_1:def_2
.= succ k by NAT_1:38 ;
then  card (k + 1) = card (succ k) ;
then omega *` (card (k + 1)) = card ((succ k) *^ omega) by Th14, CARD_1:47
.= card ((k *^ omega) +^ omega) by ORDINAL2:36
.= (card (k *^ omega)) +` omega by Th13, CARD_1:47
.= (omega *` (card k)) +` omega by Th14, CARD_1:47
.= omega by A3, Th76 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
A4: for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  omega *` (card n) c= omega ; ::_thesis: (card n) *` omega c= omega
thus  (card n) *` omega c= omega by A4; ::_thesis: verum
end;

theorem Th90: :: CARD_2:90
for K, L, M, N being Cardinal st ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) holds
( K *` M c= L *` N & M *` K c= L *` N )
proof
let K, L, M, N be Cardinal; ::_thesis: ( ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) implies ( K *` M c= L *` N & M *` K c= L *` N ) )
assume A1: ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) ; ::_thesis: ( K *` M c= L *` N & M *` K c= L *` N )
A2: K c= L by A1, CARD_1:3;
A3: M c= N by A1, CARD_1:3;
A4: K *` M = card [:K,M:] ;
A5: [:K,M:] c= [:L,N:] by A2, A3, ZFMISC_1:96;
hence  K *` M c= L *` N by CARD_1:11; ::_thesis: M *` K c= L *` N
thus  M *` K c= L *` N by A4, A5, CARD_1:11; ::_thesis: verum
end;

theorem :: CARD_2:91
for M, N, K being Cardinal st ( M in N or M c= N ) holds
( K *` M c= K *` N & K *` M c= N *` K & M *` K c= K *` N & M *` K c= N *` K ) by Th90;

theorem Th92: :: CARD_2:92
for K, L, M, N being Cardinal holds
( ( not ( K in L & M in N ) & not ( K c= L & M in N ) & not ( K in L & M c= N ) & not ( K c= L & M c= N ) ) or K = 0 or exp (K,M) c= exp (L,N) )
proof
let K, L, M, N be Cardinal; ::_thesis: ( ( not ( K in L & M in N ) & not ( K c= L & M in N ) & not ( K in L & M c= N ) & not ( K c= L & M c= N ) ) or K = 0 or exp (K,M) c= exp (L,N) )
assume A1: ( ( K in L & M in N ) or ( K c= L & M in N ) or ( K in L & M c= N ) or ( K c= L & M c= N ) ) ; ::_thesis: ( K = 0 or exp (K,M) c= exp (L,N) )
A2: K c= L by A1, CARD_1:3;
A3: M c= N by A1, CARD_1:3;
now__::_thesis:_(_not_L_<>_{}_or_K_=_0_or_exp_(K,M)_c=_exp_(L,N)_)
assume  L <> {} ; ::_thesis: ( K = 0 or exp (K,M) c= exp (L,N) )
then A4: Funcs ((N \ M),L) <> {} ;
 0 c= card (Funcs ((N \ M),L)) ;
then  0 in card (Funcs ((N \ M),L)) by A4, CARD_1:3;
then A5: nextcard (card 0) c= card (Funcs ((N \ M),L)) by CARD_1:def_3;
 0 + 1 = 1 ;
then A6: 1 c= card (Funcs ((N \ M),L)) by A5, Lm8, NAT_1:42;
A7: M misses N \ M by XBOOLE_1:79;
A8: N = M \/ (N \ M) by A3, XBOOLE_1:45;
 Funcs (M,K) c= Funcs (M,L) by A2, FUNCT_5:56;
then A9: exp (K,M) c= card (Funcs (M,L)) by CARD_1:11;
A10: exp (L,N) = card [:(Funcs (M,L)),(Funcs ((N \ M),L)):] by A7, A8, FUNCT_5:62;
A11: card [:(Funcs (M,L)),(Funcs ((N \ M),L)):] = card [:(card (Funcs (M,L))),(card (Funcs ((N \ M),L))):] by Th7;
 (card (Funcs (M,L))) *` (card (Funcs ((N \ M),L))) = card [:(card (Funcs (M,L))),(card (Funcs ((N \ M),L))):] ;
then  1 *` (card (Funcs (M,L))) c= exp (L,N) by A6, A10, A11, Th90;
then  card (Funcs (M,L)) c= exp (L,N) by Th21;
hence  ( K = 0 or exp (K,M) c= exp (L,N) ) by A9, XBOOLE_1:1; ::_thesis: verum
end;
hence  ( K = 0 or exp (K,M) c= exp (L,N) ) by A1; ::_thesis: verum
end;

theorem :: CARD_2:93
for M, N, K being Cardinal holds
( ( not M in N & not M c= N ) or K = 0 or ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) ) )
proof
let M, N, K be Cardinal; ::_thesis: ( ( not M in N & not M c= N ) or K = 0 or ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) ) )
assume that
A1: ( M in N or M c= N ) and
A2: K <> 0 ; ::_thesis: ( exp (K,M) c= exp (K,N) & exp (M,K) c= exp (N,K) )
thus  exp (K,M) c= exp (K,N) by A1, A2, Th92; ::_thesis: exp (M,K) c= exp (N,K)
 ( M = 0 implies exp (M,K) = 0 ) by A2;
hence  exp (M,K) c= exp (N,K) by A1, Th92; ::_thesis: verum
end;

theorem Th94: :: CARD_2:94
for M, N being Cardinal holds
( M c= M +` N & N c= M +` N )
proof
let M, N be Cardinal; ::_thesis: ( M c= M +` N & N c= M +` N )
A1: M c= M +^ N by ORDINAL3:24;
A2: N c= M +^ N by ORDINAL3:24;
A3: card N = N by CARD_1:def_2;
 card M = M by CARD_1:def_2;
then A4: M c= card (M +^ N) by A1, CARD_1:11;
 N c= card (M +^ N) by A2, A3, CARD_1:11;
hence  ( M c= M +` N & N c= M +` N ) by A4; ::_thesis: verum
end;

theorem :: CARD_2:95
for N, M being Cardinal st N <> 0 holds
( M c= M *` N & M c= N *` M )
proof
let N, M be Cardinal; ::_thesis: ( N <> 0 implies ( M c= M *` N & M c= N *` M ) )
assume A1: N <> 0 ; ::_thesis: ( M c= M *` N & M c= N *` M )
A2: card M = M by CARD_1:def_2;
 card N = N by CARD_1:def_2;
then A3: M *` N = card (M *^ N) by A2, Th14;
 M c= M *^ N by A1, ORDINAL3:36;
hence  ( M c= M *` N & M c= N *` M ) by A2, A3, CARD_1:11; ::_thesis: verum
end;

theorem Th96: :: CARD_2:96
for K, L, M, N being Cardinal st K in L & M in N holds
( K +` M in L +` N & M +` K in L +` N )
proof
let K, L, M, N be Cardinal; ::_thesis: ( K in L & M in N implies ( K +` M in L +` N & M +` K in L +` N ) )
A1: for K, L, M, N being Cardinal st K in L & M in N & L c= N holds
K +` M in L +` N
proof
let K, L, M, N be Cardinal; ::_thesis: ( K in L & M in N & L c= N implies K +` M in L +` N )
assume that
A2: K in L and
A3: M in N and
A4: L c= N ; ::_thesis: K +` M in L +` N
A5: now__::_thesis:_(_N_is_finite_implies_K_+`_M_in_L_+`_N_)
assume A6: N is finite ; ::_thesis: K +` M in L +` N
then reconsider N = N as finite Cardinal ;
reconsider L = L, M = M, K = K as finite Cardinal by A2, A3, A4, A6, CARD_3:92;
A7: card K = K by CARD_1:def_2;
A8: card L = L by CARD_1:def_2;
A9: card M = M by CARD_1:def_2;
A10: card N = N by CARD_1:def_2;
A11: K +` M = card ((card K) + (card M)) by A7, A9, Th38;
A12: L +` N = card ((card L) + (card N)) by A8, A10, Th38;
A13: card K < card L by A2, A7, A8, NAT_1:41;
 card M < card N by A3, A9, A10, NAT_1:41;
then  (card K) + (card M) < (card L) + (card N) by A13, XREAL_1:8;
hence  K +` M in L +` N by A11, A12, NAT_1:41; ::_thesis: verum
end;
now__::_thesis:_(_not_N_is_finite_implies_K_+`_M_in_L_+`_N_)
assume A14: not N is finite ; ::_thesis: K +` M in L +` N
then A15: L +` N = N by A4, Th76;
A16: omega c= N by A14, CARD_3:85;
 ( ( K c= M & ( M is finite or not M is finite ) ) or ( M c= K & ( K is finite or not K is finite ) ) ) ;
then A17: ( ( K is finite & M is finite ) or K +` M = M or ( K +` M = K & K in N ) ) by A2, A4, Th76;
now__::_thesis:_(_K_is_finite_&_M_is_finite_implies_K_+`_M_in_L_+`_N_)
assume that
A18: K is finite and
A19: M is finite ; ::_thesis: K +` M in L +` N
reconsider K = K, M = M as finite Cardinal by A18, A19;
A20: card K = K by CARD_1:def_2;
 card M = M by CARD_1:def_2;
then K +` M = card ((card K) + (card M)) by A20, Th38
.= (card K) + (card M) by CARD_1:def_2 ;
hence  K +` M in L +` N by A15, A16, TARSKI:def_3; ::_thesis: verum
end;
hence  K +` M in L +` N by A3, A4, A14, A17, Th76; ::_thesis: verum
end;
hence  K +` M in L +` N by A5; ::_thesis: verum
end;
 ( L c= N or N c= L ) ;
hence  ( K in L & M in N implies ( K +` M in L +` N & M +` K in L +` N ) ) by A1; ::_thesis: verum
end;

theorem :: CARD_2:97
for K, M, N being Cardinal st K +` M in K +` N holds
M in N
proof
let K, M, N be Cardinal; ::_thesis: ( K +` M in K +` N implies M in N )
assume that
A1: K +` M in K +` N and
A2: not M in N ; ::_thesis: contradiction
 N c= M by A2, CARD_1:4;
then  K +` N c= K +` M by Th83;
hence  contradiction by A1, CARD_1:4; ::_thesis: verum
end;

theorem :: CARD_2:98
for X, Y being set st (card X) +` (card Y) = card X & card Y in card X holds
card (X \ Y) = card X
proof
let X, Y be set ; ::_thesis: ( (card X) +` (card Y) = card X & card Y in card X implies card (X \ Y) = card X )
assume that
A1: (card X) +` (card Y) = card X and
A2: card Y in card X ; ::_thesis: card (X \ Y) = card X
A3: card X c= card (X \/ Y) by CARD_1:11, XBOOLE_1:7;
 card (X \/ Y) c= card X by A1, Th34;
then A4: card (X \/ Y) = card X by A3, XBOOLE_0:def_10;
 (X \ Y) \/ Y = X \/ Y by XBOOLE_1:39;
then A5: card X = (card (X \ Y)) +` (card Y) by A4, Th35, XBOOLE_1:79;
then A6: card (X \ Y) c= card X by Th94;
A7: now__::_thesis:_(_not_card_X_is_finite_implies_card_(X_\_Y)_=_card_X_)
assume  not card X is finite ; ::_thesis: card (X \ Y) = card X
then A8: (card X) +` (card X) = card X by Th75;
assume  not card (X \ Y) = card X ; ::_thesis: contradiction
then  card (X \ Y) in card X by A6, CARD_1:3;
then  card X in card X by A2, A5, A8, Th96;
hence  contradiction ; ::_thesis: verum
end;
now__::_thesis:_(_card_X_is_finite_implies_card_(X_\_Y)_=_card_X_)
assume  card X is finite ; ::_thesis: card (X \ Y) = card X
then reconsider X = X, Y = Y as finite set by A2, CARD_3:92;
 card Y = card (card Y) ;
then  card ((card X) + (card Y)) = card (card X) by A1, Th38;
then  (card X) + (card Y) = (card X) + 0 by CARD_1:40;
then  Y = {} ;
hence  card (X \ Y) = card X ; ::_thesis: verum
end;
hence  card (X \ Y) = card X by A7; ::_thesis: verum
end;

theorem :: CARD_2:99
for K, M, N being Cardinal st K *` M in K *` N holds
M in N
proof
let K, M, N be Cardinal; ::_thesis: ( K *` M in K *` N implies M in N )
assume that
A1: K *` M in K *` N and
A2: not M in N ; ::_thesis: contradiction
 N c= M by A2, CARD_1:4;
then  K *` N c= K *` M by Th90;
hence  contradiction by A1, CARD_1:4; ::_thesis: verum
end;

theorem :: CARD_2:100
for X, Y being set st X is countable & Y is countable holds
X \+\ Y is countable
proof
let X, Y be set ; ::_thesis: ( X is countable & Y is countable implies X \+\ Y is countable )
assume that
A1: X is countable and
A2: Y is countable ; ::_thesis: X \+\ Y is countable
A3: X \ Y is countable by A1;
 Y \ X is countable by A2;
hence  X \+\ Y is countable by A3, Th85; ::_thesis: verum
end;

registration
let A be finite set ;
let B be set ;
let f be Function of A,(Fin B);
cluster Union f ->  finite ;
coherence
 Union f is finite
proof
now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_
f_._x_is_finite
let x be set ; ::_thesis: ( x in dom f implies f . x is finite )
assume A1: x in dom f ; ::_thesis: f . x is finite
then reconsider A = A as non empty set ;
reconsider x9 = x as Element of A by A1;
reconsider f9 = f as Function of A,(Fin B) ;
 f9 . x9 is finite ;
hence  f . x is finite ; ::_thesis: verum
end;
hence  Union f is finite by Th88; ::_thesis: verum
end;
end;

registration
let f be finite finite-yielding Function;
cluster product f ->  finite ;
coherence
 product f is finite
proof
 Funcs ((dom f),(Union f)) is finite by FRAENKEL:6;
hence  product f is finite by FINSET_1:1, FUNCT_6:1; ::_thesis: verum
end;
end;

theorem :: CARD_2:101
for F being Function st dom F is infinite & rng F is finite holds
ex x being set st
( x in rng F & F " {x} is infinite )
proof
let F be Function; ::_thesis: ( dom F is infinite & rng F is finite implies ex x being set st
( x in rng F & F " {x} is infinite ) )
assume that
A1: dom F is infinite and
A2: rng F is finite ; ::_thesis: ex x being set st
( x in rng F & F " {x} is infinite )
deffunc H5( set ) ->  set = F " {$1};
consider g being Function such that
A3: ( dom g = rng F & ( for x being set st x in rng F holds
g . x = H5(x) ) ) from FUNCT_1:sch_3();
A4: dom F c= Union g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom F or x in Union g )
assume A5: x in dom F ; ::_thesis: x in Union g
A6: F . x in rng F by A5, FUNCT_1:def_3;
then A7: g . (F . x) in rng g by A3, FUNCT_1:def_3;
 F . x in {(F . x)} by TARSKI:def_1;
then A8: x in F " {(F . x)} by A5, FUNCT_1:def_7;
 g . (F . x) = F " {(F . x)} by A3, A6;
then  x in union (rng g) by A8, A7, TARSKI:def_4;
hence  x in Union g ; ::_thesis: verum
end;
assume A9: for x being set st x in rng F holds
F " {x} is finite ; ::_thesis: contradiction
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_is_finite
let x be set ; ::_thesis: ( x in dom g implies g . x is finite )
assume A10: x in dom g ; ::_thesis: g . x is finite
 g . x = F " {x} by A3, A10;
hence  g . x is finite by A9, A3, A10; ::_thesis: verum
end;
then  Union g is finite by A2, A3, Th88;
hence  contradiction by A1, A4; ::_thesis: verum
end;