begin
Lm1:
1 = card 1
by CARD_1:def 5;
Lm2:
2 = card 2
by CARD_1:def 5;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
begin
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem
canceled;
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
Lm3:
for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
for A being Ordinal st A in dom phi holds
( A in dom psi & phi . A = psi . A )
theorem
theorem Th20:
theorem Th21:
theorem
theorem Th23:
:: deftheorem CARD_5:def 1 :
canceled;
:: deftheorem Def2 defines cf CARD_5:def 2 :
:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :
begin
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
theorem
canceled;
theorem
canceled;
theorem Th31:
theorem
begin
:: deftheorem defines regular CARD_5:def 4 :
theorem
canceled;
theorem Th34:
Lm4:
1 = card 1
by CARD_1:def 5;
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
begin
theorem Th43:
theorem
theorem Th45:
theorem
theorem
Lm1:
for O being Ordinal
for X being finite set st X c= O holds
order_type_of (RelIncl X) is finite
theorem Th48:
theorem Th49:
theorem