:: K\"onig's Theorem
:: by Grzegorz Bancerek
::
:: Received April 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
let IT be Function;
attrIT is Cardinal-yielding  means :Def1: :: CARD_3:def 1
 for x being set st x in dom IT holds
IT . x is Cardinal;
end;

:: deftheorem Def1 defines Cardinal-yielding CARD_3:def_1_:_
 for IT being Function holds
( IT is Cardinal-yielding iff for x being set st x in dom IT holds
IT . x is Cardinal );

registration
cluster empty Relation-like Function-like  ->  Cardinal-yielding for set ;
coherence
 for b1 being Function st b1 is empty holds
b1 is Cardinal-yielding
proofend;
end;

registration
cluster Relation-like Function-like Cardinal-yielding for set ;
existence
 ex b1 being Function st b1 is Cardinal-yielding
proofend;
end;

definition
mode Cardinal-Function is Cardinal-yielding Function;
end;

registration
let ff be Cardinal-Function;
let X be set ;
clusterff | X ->  Cardinal-yielding ;
coherence
 ff | X is Cardinal-yielding
proofend;
end;

registration
let X be set ;
let K be Cardinal;
clusterX --> K ->  Cardinal-yielding ;
coherence
 X --> K is Cardinal-yielding
proofend;
end;

registration
let X be set ;
let K be Cardinal;
clusterX .--> K ->  Cardinal-yielding ;
coherence
 X .--> K is Cardinal-yielding ;
end;

scheme :: CARD_3:sch 1
CFLambda{ F1() ->  set , F2( set ) ->  Cardinal } :
 ex ff being Cardinal-Function st
( dom ff = F1() & ( for x being set st x in F1() holds
ff . x = F2(x) ) )
proofend;

definition
let f be Function;
func Card f ->  Cardinal-Function means :Def2: :: CARD_3:def 2
( dom it = dom f & ( for x being set st x in dom f holds
it . x = card (f . x) ) );
existence
 ex b1 being Cardinal-Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = card (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Cardinal-Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = card (f . x) ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = card (f . x) ) holds
b1 = b2
proofend;
func disjoin f ->  Function means :Def3: :: CARD_3:def 3
( dom it = dom f & ( for x being set st x in dom f holds
it . x = [:(f . x),{x}:] ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = [:(f . x),{x}:] ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = [:(f . x),{x}:] ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = [:(f . x),{x}:] ) holds
b1 = b2
proofend;
func Union f ->  set  equals :: CARD_3:def 4
 union (rng f);
correctness
coherence
union (rng f) is set ;
;
defpred S1[ set ] means  ex g being Function st
( $1 = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) );
func product f ->  set  means :Def5: :: CARD_3:def 5
 for x being set holds
( x in it iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) & ( for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Card CARD_3:def_2_:_
 for f being Function
for b2 being Cardinal-Function holds
( b2 = Card f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = card (f . x) ) ) );

:: deftheorem Def3 defines disjoin CARD_3:def_3_:_
 for f, b2 being Function holds
( b2 = disjoin f iff ( dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = [:(f . x),{x}:] ) ) );

:: deftheorem  defines Union CARD_3:def_4_:_
 for f being Function holds Union f = union (rng f);

:: deftheorem Def5 defines product CARD_3:def_5_:_
 for f being Function
for b2 being set holds
( b2 = product f iff for x being set holds
( x in b2 iff ex g being Function st
( x = g & dom g = dom f & ( for y being set st y in dom f holds
g . y in f . y ) ) ) );

theorem Th1: :: CARD_3:1
for ff being Cardinal-Function holds Card ff = ff
proofend;

theorem :: CARD_3:2
for X, Y being set holds Card (X --> Y) = X --> (card Y)
proofend;

theorem :: CARD_3:3
disjoin {} = {}
proofend;

theorem Th4: :: CARD_3:4
for x, X being set holds disjoin (x .--> X) = x .--> [:X,{x}:]
proofend;

theorem :: CARD_3:5
for x, y being set
for f being Function st x in dom f &amp; y in dom f &amp; x <> y holds
(disjoin f) . x misses (disjoin f) . y
proofend;

theorem Th6: :: CARD_3:6
for X, Y being set holds Union (X --> Y) c= Y
proofend;

theorem Th7: :: CARD_3:7
for X, Y being set st X <> {} holds
Union (X --> Y) = Y
proofend;

theorem :: CARD_3:8
for x, Y being set holds Union (x .--> Y) = Y by Th7;

theorem Th9: :: CARD_3:9
for g, f being Function holds
( g in product f iff ( dom g = dom f &amp; ( for x being set st x in dom f holds
g . x in f . x ) ) )
proofend;

theorem Th10: :: CARD_3:10
product {} = {{}}
proofend;

theorem Th11: :: CARD_3:11
for X, Y being set holds Funcs (X,Y) = product (X --> Y)
proofend;

defpred S1[ set ] means $1 is Function;

definition
let x, X be set ;
defpred S2[ set , set ] means  ex g being Function st
( $1 = g &amp; $2 = g . x );
func pi (X,x) ->  set  means :Def6: :: CARD_3:def 6
 for y being set holds
( y in it iff ex f being Function st
( f in X &amp; y = f . x ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ex f being Function st
( f in X &amp; y = f . x ) )
proofend;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ex f being Function st
( f in X &amp; y = f . x ) ) ) &amp; ( for y being set holds
( y in b2 iff ex f being Function st
( f in X &amp; y = f . x ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines pi CARD_3:def_6_:_
 for x, X, b3 being set holds
( b3 = pi (X,x) iff for y being set holds
( y in b3 iff ex f being Function st
( f in X &amp; y = f . x ) ) );

theorem :: CARD_3:12
for x being set
for f being Function st x in dom f &amp; product f <> {} holds
pi ((product f),x) = f . x
proofend;

theorem :: CARD_3:13
for x being set holds pi ({},x) = {}
proofend;

theorem :: CARD_3:14
for x being set
for g being Function holds pi ({g},x) = {(g . x)}
proofend;

theorem :: CARD_3:15
for x being set
for f, g being Function holds pi ({f,g},x) = {(f . x),(g . x)}
proofend;

theorem Th16: :: CARD_3:16
for X, Y, x being set holds pi ((X \/ Y),x) = (pi (X,x)) \/ (pi (Y,x))
proofend;

theorem :: CARD_3:17
for X, Y, x being set holds pi ((X /\ Y),x) c= (pi (X,x)) /\ (pi (Y,x))
proofend;

theorem Th18: :: CARD_3:18
for X, x, Y being set holds (pi (X,x)) \ (pi (Y,x)) c= pi ((X \ Y),x)
proofend;

theorem :: CARD_3:19
for X, x, Y being set holds (pi (X,x)) \+\ (pi (Y,x)) c= pi ((X \+\ Y),x)
proofend;

theorem Th20: :: CARD_3:20
for X, x being set holds card (pi (X,x)) c= card X
proofend;

theorem Th21: :: CARD_3:21
for x being set
for f being Function st x in Union (disjoin f) holds
ex y, z being set st x = [y,z]
proofend;

theorem Th22: :: CARD_3:22
for x being set
for f being Function holds
( x in Union (disjoin f) iff ( x `2 in dom f &amp; x `1 in f . (x `2) &amp; x = [(x `1),(x `2)] ) )
proofend;

theorem Th23: :: CARD_3:23
for f, g being Function st f c= g holds
disjoin f c= disjoin g
proofend;

theorem Th24: :: CARD_3:24
for f, g being Function st f c= g holds
Union f c= Union g
proofend;

theorem :: CARD_3:25
for Y, X being set holds Union (disjoin (Y --> X)) = [:X,Y:]
proofend;

theorem Th26: :: CARD_3:26
for f being Function holds
( product f = {} iff {} in rng f )
proofend;

theorem Th27: :: CARD_3:27
for f, g being Function st dom f = dom g &amp; ( for x being set st x in dom f holds
f . x c= g . x ) holds
product f c= product g
proofend;

theorem :: CARD_3:28
for F being Cardinal-Function
for x being set st x in dom F holds
card (F . x) = F . x
proofend;

theorem Th29: :: CARD_3:29
for F being Cardinal-Function
for x being set st x in dom F holds
card ((disjoin F) . x) = F . x
proofend;

definition
let F be Cardinal-Function;
func Sum F ->  Cardinal equals :: CARD_3:def 7
 card (Union (disjoin F));
correctness
coherence
card (Union (disjoin F)) is Cardinal;
;
func Product F ->  Cardinal equals :: CARD_3:def 8
 card (product F);
correctness
coherence
card (product F) is Cardinal;
;
end;

:: deftheorem  defines Sum CARD_3:def_7_:_
 for F being Cardinal-Function holds Sum F = card (Union (disjoin F));

:: deftheorem  defines Product CARD_3:def_8_:_
 for F being Cardinal-Function holds Product F = card (product F);

theorem :: CARD_3:30
for F, G being Cardinal-Function st dom F = dom G &amp; ( for x being set st x in dom F holds
F . x c= G . x ) holds
Sum F c= Sum G
proofend;

theorem :: CARD_3:31
for F being Cardinal-Function holds
( {} in rng F iff Product F = 0 )
proofend;

theorem :: CARD_3:32
for F, G being Cardinal-Function st dom F = dom G &amp; ( for x being set st x in dom F holds
F . x c= G . x ) holds
Product F c= Product G by Th27, CARD_1:11;

theorem :: CARD_3:33
for F, G being Cardinal-Function st F c= G holds
Sum F c= Sum G
proofend;

theorem :: CARD_3:34
for F, G being Cardinal-Function st F c= G &amp; not 0 in rng G holds
Product F c= Product G
proofend;

theorem :: CARD_3:35
for K being Cardinal holds Sum ({} --> K) = 0
proofend;

theorem :: CARD_3:36
for K being Cardinal holds Product ({} --> K) = 1 by Th10, CARD_1:30;

theorem :: CARD_3:37
for K being Cardinal
for x being set holds Sum (x .--> K) = K
proofend;

theorem :: CARD_3:38
for K being Cardinal
for x being set holds Product (x .--> K) = K
proofend;

theorem Th39: :: CARD_3:39
for f being Function holds card (Union f) c= Sum (Card f)
proofend;

theorem :: CARD_3:40
for F being Cardinal-Function holds card (Union F) c= Sum F
proofend;

:: [WP: ] Koenig_Theorem
theorem :: CARD_3:41
for F, G being Cardinal-Function st dom F = dom G &amp; ( for x being set st x in dom F holds
F . x in G . x ) holds
Sum F in Product G
proofend;

scheme :: CARD_3:sch 2
FuncSeparation{ F1() ->  set , F2( set ) ->  set , P1[ set , set ] } :
 ex f being Function st
( dom f = F1() &amp; ( for x being set st x in F1() holds
for y being set holds
( y in f . x iff ( y in F2(x) &amp; P1[x,y] ) ) ) )
proofend;

Lm1:  for x being set
for R being Relation st x in field R holds
ex y being set st
( [x,y] in R or [y,x] in R )
proofend;

theorem Th42: :: CARD_3:42
for X being set st X is finite holds
card X in card omega
proofend;

theorem Th43: :: CARD_3:43
for A, B being Ordinal st card A in card B holds
A in B
proofend;

theorem Th44: :: CARD_3:44
for A being Ordinal
for M being Cardinal st card A in M holds
A in M
proofend;

theorem Th45: :: CARD_3:45
for X being set st X is c=-linear holds
ex Y being set st
( Y c= X &amp; union Y = union X &amp; ( for Z being set st Z c= Y &amp; Z <> {} holds
ex Z1 being set st
( Z1 in Z &amp; ( for Z2 being set st Z2 in Z holds
Z1 c= Z2 ) ) ) )
proofend;

theorem :: CARD_3:46
for M being Cardinal
for X being set st ( for Z being set st Z in X holds
card Z in M ) &amp; X is c=-linear holds
card (union X) c= M
proofend;

begin

:: from AMI_1
registration
let f be Function;
cluster product f ->  functional ;
coherence
 product f is functional
proofend;
end;

registration
let A be set ;
let B be with_non-empty_elements set ;
cluster Function-like quasi_total  ->  non-empty for Element of bool [:A,B:];
coherence
 for b1 being Function of A,B holds b1 is non-empty
proofend;
end;

:: from PRVECT_1
registration
let f be non-empty Function;
cluster product f ->  non empty ;
coherence
 not product f is empty
proofend;
end;

:: from AMI_1, 2006.03.14, A.T.
theorem :: CARD_3:47
for a, b, c, d being set st a <> b holds
product ((a,b) --> ({c},{d})) = {((a,b) --> (c,d))}
proofend;

:: from AMI_1, 2006.03.14, A.T.
theorem :: CARD_3:48
for x being set
for f being Function st x in product f holds
x is Function ;

begin

definition
let f be Function;
func sproduct f ->  set  means :Def9: :: CARD_3:def 9
 for x being set holds
( x in it iff ex g being Function st
( x = g &amp; dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex g being Function st
( x = g &amp; dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex g being Function st
( x = g &amp; dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) &amp; ( for x being set holds
( x in b2 iff ex g being Function st
( x = g &amp; dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines sproduct CARD_3:def_9_:_
 for f being Function
for b2 being set holds
( b2 = sproduct f iff for x being set holds
( x in b2 iff ex g being Function st
( x = g &amp; dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) ) ) );

registration
let f be Function;
cluster sproduct f ->  non empty functional ;
coherence
 ( sproduct f is functional &amp; not sproduct f is empty )
proofend;
end;

theorem Th49: :: CARD_3:49
for g, f being Function st g in sproduct f holds
( dom g c= dom f &amp; ( for x being set st x in dom g holds
g . x in f . x ) )
proofend;

theorem Th50: :: CARD_3:50
for f being Function holds {} in sproduct f
proofend;

registration
let f be Function;
cluster empty Relation-like Function-like for Element of sproduct f;
existence
 ex b1 being Element of sproduct f st b1 is empty
proofend;
end;

theorem Th51: :: CARD_3:51
for f being Function holds product f c= sproduct f
proofend;

theorem Th52: :: CARD_3:52
for x being set
for f being Function st x in sproduct f holds
x is PartFunc of (dom f),(union (rng f))
proofend;

theorem Th53: :: CARD_3:53
for g, f, h being Function st g in product f &amp; h in sproduct f holds
g +* h in product f
proofend;

theorem :: CARD_3:54
for f, g being Function st product f <> {} holds
( g in sproduct f iff ex h being Function st
( h in product f &amp; g c= h ) )
proofend;

theorem Th55: :: CARD_3:55
for f being Function holds sproduct f c= PFuncs ((dom f),(union (rng f)))
proofend;

theorem Th56: :: CARD_3:56
for f, g being Function st f c= g holds
sproduct f c= sproduct g
proofend;

theorem Th57: :: CARD_3:57
sproduct {} = {{}}
proofend;

theorem :: CARD_3:58
for A, B being set holds PFuncs (A,B) = sproduct (A --> B)
proofend;

theorem :: CARD_3:59
for A, B being non empty set
for f being Function of A,B holds sproduct f = sproduct (f |  {  x where x is Element of A : f . x <> {}  }  )
proofend;

theorem Th60: :: CARD_3:60
for x, y being set
for f being Function st x in dom f &amp; y in f . x holds
x .--> y in sproduct f
proofend;

theorem :: CARD_3:61
for f being Function holds
( sproduct f = {{}} iff for x being set st x in dom f holds
f . x = {} )
proofend;

theorem Th62: :: CARD_3:62
for f being Function
for A being set st A c= sproduct f &amp; ( for h1, h2 being Function st h1 in A &amp; h2 in A holds
h1 tolerates h2 ) holds
union A in sproduct f
proofend;

theorem :: CARD_3:63
for g, h, f being Function st g tolerates h &amp; g in sproduct f &amp; h in sproduct f holds
g \/ h in sproduct f
proofend;

theorem Th64: :: CARD_3:64
for x being set
for h, f being Function st x c= h &amp; h in sproduct f holds
x in sproduct f
proofend;

theorem Th65: :: CARD_3:65
for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct f by Th64, RELAT_1:59;

theorem Th66: :: CARD_3:66
for g, f being Function
for A being set st g in sproduct f holds
g | A in sproduct (f | A)
proofend;

theorem :: CARD_3:67
for h, f, g being Function st h in sproduct (f +* g) holds
ex f9, g9 being Function st
( f9 in sproduct f &amp; g9 in sproduct g &amp; h = f9 +* g9 )
proofend;

theorem Th68: :: CARD_3:68
for g, f, f9, g9 being Function st dom g misses (dom f9) \ (dom g9) &amp; f9 in sproduct f &amp; g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
proofend;

theorem :: CARD_3:69
for g, f, f9, g9 being Function st dom f9 misses (dom g) \ (dom g9) &amp; f9 in sproduct f &amp; g9 in sproduct g holds
f9 +* g9 in sproduct (f +* g)
proofend;

theorem Th70: :: CARD_3:70
for g, f, h being Function st g in sproduct f &amp; h in sproduct f holds
g +* h in sproduct f
proofend;

theorem :: CARD_3:71
for f being Function
for x1, x2, y1, y2 being set st x1 in dom f &amp; y1 in f . x1 &amp; x2 in dom f &amp; y2 in f . x2 holds
(x1,x2) --> (y1,y2) in sproduct f
proofend;

begin

definition
let IT be set ;
attrIT is with_common_domain  means :Def10: :: CARD_3:def 10
 for f, g being Function st f in IT &amp; g in IT holds
dom f = dom g;
end;

:: deftheorem Def10 defines with_common_domain CARD_3:def_10_:_
 for IT being set holds
( IT is with_common_domain iff for f, g being Function st f in IT &amp; g in IT holds
dom f = dom g );

registration
cluster non empty functional with_common_domain for set ;
existence
 ex b1 being set st
( b1 is with_common_domain &amp; b1 is functional &amp; not b1 is empty )
proofend;
end;

registration
let f be Function;
cluster{f} ->  with_common_domain ;
coherence
 {f} is with_common_domain
proofend;
end;

definition
let X be functional set ;
func DOM X ->  set  equals :: CARD_3:def 11
 meet  {  (dom f) where f is Element of X : verum  }  ;
coherence
 meet  {  (dom f) where f is Element of X : verum  }  is set ;
end;

:: deftheorem  defines DOM CARD_3:def_11_:_
 for X being functional set holds DOM X = meet  {  (dom f) where f is Element of X : verum  }  ;

LmX:  for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X
proofend;

theorem Th72: :: CARD_3:72
for X being functional with_common_domain set st X = {{}} holds
DOM X = {}
proofend;

registration
let X be empty set ;
cluster DOM X ->  empty ;
coherence
 DOM X is empty
proofend;
end;

begin

definition
let S be functional set ;
func product" S ->  Function means :Def12: :: CARD_3:def 12
( dom it = DOM S &amp; ( for i being set st i in dom it holds
it . i = pi (S,i) ) );
existence
 ex b1 being Function st
( dom b1 = DOM S &amp; ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = DOM S &amp; ( for i being set st i in dom b1 holds
b1 . i = pi (S,i) ) &amp; dom b2 = DOM S &amp; ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines product" CARD_3:def_12_:_
 for S being functional set
for b2 being Function holds
( b2 = product" S iff ( dom b2 = DOM S &amp; ( for i being set st i in dom b2 holds
b2 . i = pi (S,i) ) ) );

theorem :: CARD_3:73
canceled;

theorem Th74: :: CARD_3:74
for S being non empty functional set
for i being set st i in dom (product" S) holds
(product" S) . i =  {  (f . i) where f is Element of S : verum  }
proofend;

definition
let S be set ;
attrS is product-like  means :Def13: :: CARD_3:def 13
 ex f being Function st S = product f;
end;

:: deftheorem Def13 defines product-like CARD_3:def_13_:_
 for S being set holds
( S is product-like iff ex f being Function st S = product f );

registration
let f be Function;
cluster product f ->  product-like ;
coherence
 product f is product-like by Def13;
end;

registration
cluster product-like  ->  functional with_common_domain for set ;
coherence
 for b1 being set st b1 is product-like holds
( b1 is functional &amp; b1 is with_common_domain )
proofend;
end;

registration
cluster non empty product-like for set ;
existence
 ex b1 being set st
( b1 is product-like &amp; not b1 is empty )
proofend;
end;

theorem :: CARD_3:75
canceled;

theorem :: CARD_3:76
canceled;

theorem Th77: :: CARD_3:77
for S being functional with_common_domain set holds S c= product (product" S)
proofend;

theorem :: CARD_3:78
for S being non empty product-like set holds S = product (product" S)
proofend;

:: from AMI_1, 2008.04.11, A.T. (generalized)
theorem :: CARD_3:79
for f being Function
for s, t being Element of product f
for A being set holds s +* (t | A) is Element of product f
proofend;

theorem :: CARD_3:80
for f being non-empty Function
for p being Element of sproduct f ex s being Element of product f st p c= s
proofend;

theorem Th81: :: CARD_3:81
for g, f being Function
for A being set st g in product f holds
g | A in sproduct f
proofend;

:: needed, 2008.04.20, A.T.
definition
let f be non-empty Function;
let g be Element of product f;
let X be set ;
:: original:|
redefine funcg | X ->  Element of sproduct f;
coherence
 g | X is Element of sproduct f by Th81;
end;

theorem :: CARD_3:82
for f being non-empty Function
for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A
proofend;

:: from PRE_CIRC, 2008.06.02, A.T.
theorem :: CARD_3:83
for M, x, g being Function st x in product M holds
x * g in product (M * g)
proofend;

:: moved from CARD_4, 2008.10.08, A.T.
theorem :: CARD_3:84
for X being set holds
( X is finite iff card X in omega ) by Th42, CARD_1:47;

theorem Th85: :: CARD_3:85
for A being Ordinal holds
( A is infinite iff omega c= A )
proofend;

theorem :: CARD_3:86
for N, M being Cardinal st N is finite &amp; not M is finite holds
( N in M &amp; N c= M )
proofend;

theorem :: CARD_3:87
for X being set holds
( not X is finite iff ex Y being set st
( Y c= X &amp; card Y = omega ) )
proofend;

theorem Th88: :: CARD_3:88
for X, Y being set holds
( card X = card Y iff nextcard X = nextcard Y )
proofend;

theorem :: CARD_3:89
for N, M being Cardinal st nextcard N = nextcard M holds
M = N
proofend;

theorem Th90: :: CARD_3:90
for N, M being Cardinal holds
( N in M iff nextcard N c= M )
proofend;

theorem :: CARD_3:91
for N, M being Cardinal holds
( N in nextcard M iff N c= M )
proofend;

theorem :: CARD_3:92
for M, N being Cardinal st M is finite &amp; ( N c= M or N in M ) holds
N is finite
proofend;

definition
let X be set ;
attrX is countable  means :Def14: :: CARD_3:def 14
 card X c= omega ;
attrX is denumerable  means :: CARD_3:def 15
 card X = omega ;
end;

:: deftheorem Def14 defines countable CARD_3:def_14_:_
 for X being set holds
( X is countable iff card X c= omega );

:: deftheorem  defines denumerable CARD_3:def_15_:_
 for X being set holds
( X is denumerable iff card X = omega );

registration
cluster denumerable  ->  infinite countable for set ;
coherence
 for b1 being set st b1 is denumerable holds
( b1 is countable &amp; b1 is infinite )
proofend;
cluster infinite countable  ->  denumerable for set ;
coherence
 for b1 being set st b1 is countable &amp; b1 is infinite holds
b1 is denumerable
proofend;
end;

registration
cluster finite  ->  countable for set ;
coherence
 for b1 being set st b1 is finite holds
b1 is countable
proofend;
end;

registration
cluster omega  ->  denumerable ;
coherence
 omega is denumerable
proofend;
end;

registration
cluster denumerable for set ;
existence
 ex b1 being set st b1 is denumerable
proofend;
end;

theorem Th93: :: CARD_3:93
for X being set holds
( X is countable iff ex f being Function st
( dom f = omega &amp; X c= rng f ) )
proofend;

registration
let X be countable set ;
cluster  ->  countable for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is countable
proofend;
end;

Lm2:  for Y, X being set st Y c= X &amp; X is countable holds
Y is countable
;

theorem :: CARD_3:94
for X, Y being set st X is countable holds
X /\ Y is countable by Lm2, XBOOLE_1:17;

theorem :: CARD_3:95
for X, Y being set st X is countable holds
X \ Y is countable ;

theorem :: CARD_3:96
for A being non empty countable set ex f being Function of omega,A st rng f = A
proofend;

:: from CIRCCOMB, 2009.01.26, A.T.
theorem :: CARD_3:97
for f, g being non-empty Function
for x being Element of product f
for y being Element of product g holds x +* y in product (f +* g)
proofend;

theorem :: CARD_3:98
for f, g being non-empty Function
for x being Element of product (f +* g) holds x | (dom g) in product g
proofend;

theorem :: CARD_3:99
for f, g being non-empty Function st f tolerates g holds
for x being Element of product (f +* g) holds x | (dom f) in product f
proofend;

:: missing, 2009.09.06, A.T.
theorem Th100: :: CARD_3:100
for S being functional with_common_domain set
for f being Function st f in S holds
dom f = dom (product" S)
proofend;

theorem Th101: :: CARD_3:101
for S being functional set
for f being Function
for i being set st f in S &amp; i in dom (product" S) holds
f . i in (product" S) . i
proofend;

theorem :: CARD_3:102
for S being functional with_common_domain set
for f being Function
for i being set st f in S &amp; i in dom f holds
f . i in (product" S) . i
proofend;

:: 2009.09.12, A.T.
registration
let X be with_common_domain set ;
cluster  ->  with_common_domain for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is with_common_domain
proofend;
end;

:: from PRALG_3, 2009.09.18, A.T.
definition
let f be Function;
let x be set ;
func proj (f,x) ->  Function means :Def16: :: CARD_3:def 16
( dom it = product f &amp; ( for y being Function st y in dom it holds
it . y = y . x ) );
existence
 ex b1 being Function st
( dom b1 = product f &amp; ( for y being Function st y in dom b1 holds
b1 . y = y . x ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = product f &amp; ( for y being Function st y in dom b1 holds
b1 . y = y . x ) &amp; dom b2 = product f &amp; ( for y being Function st y in dom b2 holds
b2 . y = y . x ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines proj CARD_3:def_16_:_
 for f being Function
for x being set
for b3 being Function holds
( b3 = proj (f,x) iff ( dom b3 = product f &amp; ( for y being Function st y in dom b3 holds
b3 . y = y . x ) ) );

registration
let f be Function;
let x be set ;
cluster proj (f,x) ->  product f -defined ;
coherence
 proj (f,x) is product f -defined
proofend;
end;

registration
let f be Function;
let x be set ;
cluster proj (f,x) ->  total ;
coherence
 proj (f,x) is total
proofend;
end;

registration
let f be non-empty Function;
cluster  -> f -compatible for Element of product f;
coherence
 for b1 being Element of product f holds b1 is f -compatible
proofend;
end;

registration
let I be set ;
let f be non-empty I -defined Function;
cluster  -> I -defined for Element of product f;
coherence
 for b1 being Element of product f holds b1 is I -defined ;
end;

registration
let f be Function;
cluster  -> f -compatible for Element of sproduct f;
coherence
 for b1 being Element of sproduct f holds b1 is f -compatible
proofend;
end;

registration
let I be set ;
let f be I -defined Function;
cluster  -> I -defined for Element of sproduct f;
coherence
 for b1 being Element of sproduct f holds b1 is I -defined ;
end;

registration
let I be set ;
let f be non-empty I -defined total Function;
cluster  ->  total for Element of product f;
coherence
 for b1 being Element of product f holds b1 is total
proofend;
end;

theorem Th103: :: CARD_3:103
for I being set
for f being non-empty b1 -defined Function
for p being b1 -defined b2 -compatible Function holds p in sproduct f
proofend;

theorem :: CARD_3:104
for I being set
for f being non-empty b1 -defined Function
for p being b1 -defined b2 -compatible Function ex s being Element of product f st p c= s
proofend;

:: from AMISTD_2, 2010.01.10, A.T
registration
let X be infinite set ;
let a be set ;
clusterX --> a ->  infinite ;
coherence
 not X --> a is finite ;
end;

registration
cluster Relation-like Function-like infinite for set ;
existence
 ex b1 being Function st b1 is infinite
proofend;
end;

registration
let R be infinite Relation;
cluster field R ->  infinite ;
coherence
 not field R is finite by ORDERS_1:86;
end;

registration
let X be infinite set ;
cluster RelIncl X ->  infinite ;
coherence
 not RelIncl X is finite by CARD_1:63;
end;

theorem :: CARD_3:105
for R, S being Relation st R,S are_isomorphic &amp; R is finite holds
S is finite
proofend;

theorem :: CARD_3:106
product" {{}} = {}
proofend;

theorem Th107: :: CARD_3:107
for I being set
for f being V8() ManySortedSet of I
for s being b2 -compatible ManySortedSet of I holds s in product f
proofend;

registration
let I be set ;
let f be V8() ManySortedSet of I;
cluster  ->  total for Element of product f;
coherence
 for b1 being Element of product f holds b1 is total ;
end;

definition
let I be set ;
let f be V8() ManySortedSet of I;
let M be f -compatible ManySortedSet of I;
func down M ->  Element of product f equals :: CARD_3:def 17
M;
coherence
 M is Element of product f by Th107;
end;

:: deftheorem  defines down CARD_3:def_17_:_
 for I being set
for f being V8() ManySortedSet of I
for M being b2 -compatible ManySortedSet of I holds down M = M;

theorem :: CARD_3:108
for X being functional with_common_domain set
for f being Function st f in X holds
dom f = DOM X by LmX;

theorem :: CARD_3:109
for x being set
for X being non empty functional set st ( for f being Function st f in X holds
x in dom f ) holds
x in DOM X
proofend;