:: CARD_5 semantic presentation
Lemma1:
( 0 = Card 0 & 1 = Card 1 & 2 = Card 2 )
by CARD_1:def 5;
theorem Th1: :: CARD_5:1
theorem Th2: :: CARD_5:2
canceled;
theorem Th3: :: CARD_5:3
canceled;
theorem Th4: :: CARD_5:4
canceled;
theorem Th5: :: CARD_5:5
canceled;
theorem Th6: :: CARD_5:6
canceled;
theorem Th7: :: CARD_5:7
canceled;
theorem Th8: :: CARD_5:8
theorem Th9: :: CARD_5:9
theorem Th10: :: CARD_5:10
theorem Th11: :: CARD_5:11
theorem Th12: :: CARD_5:12
theorem Th13: :: CARD_5:13
theorem Th14: :: CARD_5:14
theorem Th15: :: CARD_5:15
theorem Th16: :: CARD_5:16
theorem Th17: :: CARD_5:17
theorem Th18: :: CARD_5:18
Lemma11:
for b1, b2 being Ordinal-Sequence st rng b1 = rng b2 & b1 is increasing & b2 is increasing holds
for b3 being Ordinal st b3 in dom b1 holds
( b3 in dom b2 & b1 . b3 = b2 . b3 )
theorem Th19: :: CARD_5:19
theorem Th20: :: CARD_5:20
theorem Th21: :: CARD_5:21
theorem Th22: :: CARD_5:22
theorem Th23: :: CARD_5:23
:: deftheorem Def1 CARD_5:def 1 :
canceled;
:: deftheorem Def2 defines cf CARD_5:def 2 :
:: deftheorem Def3 defines -powerfunc_of CARD_5:def 3 :
theorem Th24: :: CARD_5:24
theorem Th25: :: CARD_5:25
theorem Th26: :: CARD_5:26
theorem Th27: :: CARD_5:27
theorem Th28: :: CARD_5:28
theorem Th29: :: CARD_5:29
canceled;
theorem Th30: :: CARD_5:30
canceled;
theorem Th31: :: CARD_5:31
theorem Th32: :: CARD_5:32
:: deftheorem Def4 defines regular CARD_5:def 4 :
theorem Th33: :: CARD_5:33
canceled;
theorem Th34: :: CARD_5:34
theorem Th35: :: CARD_5:35
theorem Th36: :: CARD_5:36
theorem Th37: :: CARD_5:37
theorem Th38: :: CARD_5:38
theorem Th39: :: CARD_5:39
theorem Th40: :: CARD_5:40
theorem Th41: :: CARD_5:41
theorem Th42: :: CARD_5:42
theorem Th43: :: CARD_5:43
theorem Th44: :: CARD_5:44
theorem Th45: :: CARD_5:45
theorem Th46: :: CARD_5:46
theorem Th47: :: CARD_5:47