for K, L, M, N being Cardinal st ( ( K <` L & M <` N ) or ( K <=` L & M <` N ) or ( K <` L & M <=` N ) or ( K <=` L & M <=` N ) ) holds
( K +` M <=` L +` N & M +` K <=` L +` N )

proof end;

theorem :: CARD_4:42

for M, N, K being Cardinal st ( M <` N or M <=` N ) holds
( K +` M <=` K +` N & K +` M <=` N +` K & M +` K <=` K +` N & M +` K <=` N +` K ) by Th41;

definition

let X be set ;
attr X is countable means :Def1: :: CARD_4:def 1
Card X <=` alef 0;

end;

:: deftheorem Def1 defines countable CARD_4:def 1 :

theorem Th43: :: CARD_4:43

for X being set st X is finite holds
X is countable

proof end;

theorem Th44: :: CARD_4:44

( omega is countable & NAT is countable )

proof end;

theorem Th45: :: CARD_4:45

for X being set holds
( X is countable iff ex f being Function st
( dom f = NAT & X c= rng f ) )

proof end;

theorem Th46: :: CARD_4:46

for Y, X being set st Y c= X & X is countable holds
Y is countable

proof end;

theorem Th47: :: CARD_4:47

for X, Y being set st X is countable & Y is countable holds
X \/ Y is countable

proof end;

theorem :: CARD_4:48

for X, Y being set st X is countable holds
( X /\ Y is countable & Y /\ X is countable )

proof end;

theorem Th49: :: CARD_4:49

for X, Y being set st X is countable holds
X \ Y is countable

proof end;

theorem :: CARD_4:50

for X, Y being set st X is countable & Y is countable holds
X \+\ Y is countable

proof end;

theorem Th51: :: CARD_4:51

for n being Nat
for r being Real holds
( ( r <> 0 or n = 0 ) iff r |^ n <> 0 )

proof end;

definition

let m, n be Nat;
:: original: |^
redefine func m |^ n -> Nat;
coherence

proof end;

end;

Lm2: for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
n1 <= n2

proof end;

theorem Th52: :: CARD_4:52

for n1, m1, n2, m2 being Nat st (2 |^ n1) * ((2 * m1) + 1) = (2 |^ n2) * ((2 * m2) + 1) holds
( n1 = n2 & m1 = m2 )

proof end;

Lm3: for x being set st x in [:NAT ,NAT :] holds
ex n1, n2 being Nat st x = [n1,n2]

proof end;

theorem Th53: :: CARD_4:53

( [:NAT ,NAT :], NAT are_equipotent & Card NAT = Card [:NAT ,NAT :] )

proof end;

theorem Th54: :: CARD_4:54

(alef 0) *` (alef 0) = alef 0 by Th53, CARD_1:83, CARD_1:84, CARD_2:def 2;

theorem Th55: :: CARD_4:55

for X, Y being set st X is countable & Y is countable holds
[:X,Y:] is countable

proof end;

theorem Th56: :: CARD_4:56

for D being non empty set holds
( 1 -tuples_on D,D are_equipotent & Card (1 -tuples_on D) = Card D )

proof end;

theorem Th57: :: CARD_4:57

for D being non empty set
for n, m being Nat holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & Card [:(n -tuples_on D),(m -tuples_on D):] = Card ((n + m) -tuples_on D) )

proof end;

theorem Th58: :: CARD_4:58

for D being non empty set
for n being Nat st D is countable holds
n -tuples_on D is countable

proof end;

theorem Th59: :: CARD_4:59

for M, N being Cardinal
for f being Function st Card (dom f) <=` M & ( for x being set st x in dom f holds
Card (f . x) <=` N ) holds
Card (Union f) <=` M *` N

proof end;

theorem Th60: :: CARD_4:60

for X being set
for M, N being Cardinal st Card X <=` M & ( for Y being set st Y in X holds
Card Y <=` N ) holds
Card (union X) <=` M *` N

proof end;

theorem Th61: :: CARD_4:61

for f being Function st dom f is countable & ( for x being set st x in dom f holds
f . x is countable ) holds
Union f is countable

proof end;

theorem :: CARD_4:62

for X being set st X is countable & ( for Y being set st Y in X holds
Y is countable ) holds
union X is countable

proof end;

theorem :: CARD_4:63

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 end;

theorem :: CARD_4:64

canceled;

theorem :: CARD_4:65

for D being non empty set st D is countable holds
D * is countable

proof end;

theorem :: CARD_4:66

for D being non empty set holds alef 0 <=` Card (D * )

proof end;

scheme :: CARD_4:sch 1
FraenCoun1{ F₁( set ) -> set , P₁[ Nat] } :

{ F₁(n) where n is Nat : P₁[n] } is countable

proof end;

scheme :: CARD_4:sch 2
FraenCoun2{ F₁( set , set ) -> set , P₁[ set , set ] } :

{ F₁(n1,n2) where n1, n2 is Nat : P₁[n1,n2] } is countable

proof end;

scheme :: CARD_4:sch 3
FraenCoun3{ F₁( set , set , set ) -> set , P₁[ Nat, Nat, Nat] } :

{ F₁(n1,n2,n3) where n1, n2, n3 is Nat : P₁[n1,n2,n3] } is countable

proof end;

theorem Th67: :: CARD_4:67

for n being Nat holds
( (alef 0) *` (Card n) <=` alef 0 & (Card n) *` (alef 0) <=` alef 0 )

proof end;

theorem Th68: :: CARD_4:68

for K, L, M, N being Cardinal st ( ( K <` L & M <` N ) or ( K <=` L & M <` N ) or ( K <` L & M <=` N ) or ( K <=` L & M <=` N ) ) holds
( K *` M <=` L *` N & M *` K <=` L *` N )

proof end;

theorem :: CARD_4:69

for M, N, K being Cardinal st ( M <` N or M <=` N ) holds
( K *` M <=` K *` N & K *` M <=` N *` K & M *` K <=` K *` N & M *` K <=` N *` K ) by Th68;

theorem Th70: :: CARD_4:70

for K, L, M, N being Cardinal holds
( ( not ( K <` L & M <` N ) & not ( K <=` L & M <` N ) & not ( K <` L & M <=` N ) & not ( K <=` L & M <=` N ) ) or K = 0 or exp K,M <=` exp L,N )

proof end;

theorem :: CARD_4:71

for M, N, K being Cardinal holds
( ( not M <` N & not M <=` N ) or K = 0 or ( exp K,M <=` exp K,N & exp M,K <=` exp N,K ) )

proof end;

theorem Th72: :: CARD_4:72

for M, N being Cardinal holds
( M <=` M +` N & N <=` M +` N )

proof end;

theorem :: CARD_4:73

for N, M being Cardinal st N <> 0 holds
( M <=` M *` N & M <=` N *` M )

proof end;

theorem Th74: :: CARD_4:74

for K, L, M, N being Cardinal st K <` L & M <` N holds
( K +` M <` L +` N & M +` K <` L +` N )

proof end;

theorem :: CARD_4:75

for K, M, N being Cardinal st K +` M <` K +` N holds
M <` N

proof end;

theorem Th76: :: CARD_4:76

for X, Y being set st (Card X) +` (Card Y) = Card X & Card Y <` Card X holds
Card (X \ Y) = Card X

proof end;

theorem Th77: :: CARD_4:77

for M being Cardinal st not M is finite holds
M *` M = M

proof end;

theorem Th78: :: CARD_4:78

for M, N being Cardinal st not M is finite & 0 <` N & ( N <=` M or N <` M ) holds
( M *` N = M & N *` M = M )

proof end;

theorem Th79: :: CARD_4:79

for M, N being Cardinal st not M is finite & ( N <=` M or N <` M ) holds
( M *` N <=` M & N *` M <=` M )

proof end;

theorem :: CARD_4:80

for X being set st not X is finite holds
( [:X,X:],X are_equipotent & Card [:X,X:] = Card X )

proof end;

theorem :: CARD_4:81

for X, Y being set st not X is finite & Y is finite & Y <> {} holds
( [:X,Y:],X are_equipotent & Card [:X,Y:] = Card X )

proof end;

theorem :: CARD_4:82

for K, L, M, N being Cardinal st K <` L & M <` N holds
( K *` M <` L *` N & M *` K <` L *` N )

proof end;

theorem :: CARD_4:83

for K, M, N being Cardinal st K *` M <` K *` N holds
M <` N

proof end;

theorem Th84: :: CARD_4:84

for X being set st not X is finite holds
Card X = (alef 0) *` (Card X)

proof end;

theorem :: CARD_4:85

for X, Y being set st X <> {} & X is finite & not Y is finite holds
(Card Y) *` (Card X) = Card Y

proof end;

theorem Th86: :: CARD_4:86

for D being non empty set
for n being Nat st not D is finite & n <> 0 holds
( n -tuples_on D,D are_equipotent & Card (n -tuples_on D) = Card D )

proof end;

theorem :: CARD_4:87

for D being non empty set st not D is finite holds
Card D = Card (D * )

proof end;