let c₁ be Ordinal;
let c₂ be Ordinal-Sequence;
canceled;
func c₁ +^ c₂ -> Ordinal-Sequence means :Def2: :: ORDINAL3:def 2
( dom a₃ = dom a₂ & ( for b₁ being Ordinal st b₁ in dom a₂ holds
a₃ . b₁ = a₁ +^ (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func c₂ +^ c₁ -> Ordinal-Sequence means :: ORDINAL3:def 3
( dom a₃ = dom a₂ & ( for b₁ being Ordinal st b₁ in dom a₂ holds
a₃ . b₁ = (a₂ . b₁) +^ a₁ ) );
existence

proof end;

uniqueness

proof end;

func c₁ *^ c₂ -> Ordinal-Sequence means :: ORDINAL3:def 4
( dom a₃ = dom a₂ & ( for b₁ being Ordinal st b₁ in dom a₂ holds
a₃ . b₁ = a₁ *^ (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

func c₂ *^ c₁ -> Ordinal-Sequence means :Def5: :: ORDINAL3:def 5
( dom a₃ = dom a₂ & ( for b₁ being Ordinal st b₁ in dom a₂ holds
a₃ . b₁ = (a₂ . b₁) *^ a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 ORDINAL3:def 1 :

:: deftheorem Def2 defines +^ ORDINAL3:def 2 :

:: deftheorem Def3 defines +^ ORDINAL3:def 3 :

:: deftheorem Def4 defines *^ ORDINAL3:def 4 :

:: deftheorem Def5 defines *^ ORDINAL3:def 5 :

theorem Th43: :: ORDINAL3:43

canceled;

theorem Th44: :: ORDINAL3:44

canceled;

theorem Th45: :: ORDINAL3:45

canceled;

theorem Th46: :: ORDINAL3:46

canceled;

theorem Th47: :: ORDINAL3:47

for b₁, b₂ being Ordinal-Sequence
for b₃ being Ordinal st {} <> dom b₁ & dom b₁ = dom b₂ & ( for b₄, b₅ being Ordinal st b₄ in dom b₁ & b₅ = b₁ . b₄ holds
b₂ . b₄ = b₃ +^ b₅ ) holds
sup b₂ = b₃ +^ (sup b₁)

proof end;

theorem Th48: :: ORDINAL3:48

for b₁, b₂ being Ordinal st b₁ is_limit_ordinal holds
b₁ *^ b₂ is_limit_ordinal

proof end;

theorem Th49: :: ORDINAL3:49

for b₁, b₂, b₃ being Ordinal st b₁ in b₂ *^ b₃ & b₂ is_limit_ordinal holds
ex b₄ being Ordinal st
( b₄ in b₂ & b₁ in b₄ *^ b₃ )

proof end;

theorem Th50: :: ORDINAL3:50

for b₁, b₂ being Ordinal-Sequence
for b₃ being Ordinal st {} <> dom b₁ & dom b₁ = dom b₂ & b₃ <> {} & sup b₁ is_limit_ordinal & ( for b₄, b₅ being Ordinal st b₄ in dom b₁ & b₅ = b₁ . b₄ holds
b₂ . b₄ = b₅ *^ b₃ ) holds
sup b₂ = (sup b₁) *^ b₃

proof end;

theorem Th51: :: ORDINAL3:51

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st {} <> dom b₁ holds
sup (b₂ +^ b₁) = b₂ +^ (sup b₁)

proof end;

theorem Th52: :: ORDINAL3:52

for b₁ being Ordinal-Sequence
for b₂ being Ordinal st {} <> dom b₁ & b₂ <> {} & sup b₁ is_limit_ordinal holds
sup (b₁ *^ b₂) = (sup b₁) *^ b₂

proof end;

theorem Th53: :: ORDINAL3:53

for b₁, b₂ being Ordinal st b₁ <> {} holds
union (b₂ +^ b₁) = b₂ +^ (union b₁)

proof end;

theorem Th54: :: ORDINAL3:54

for b₁, b₂, b₃ being Ordinal holds (b₁ +^ b₂) *^ b₃ = (b₁ *^ b₃) +^ (b₂ *^ b₃)

proof end;

theorem Th55: :: ORDINAL3:55

for b₁, b₂ being Ordinal st b₁ <> {} holds
ex b₃, b₄ being Ordinal st
( b₂ = (b₃ *^ b₁) +^ b₄ & b₄ in b₁ )

proof end;

theorem Th56: :: ORDINAL3:56

for b₁, b₂, b₃, b₄, b₅ being Ordinal st (b₂ *^ b₁) +^ b₃ = (b₄ *^ b₁) +^ b₅ & b₃ in b₁ & b₅ in b₁ holds
( b₂ = b₄ & b₃ = b₅ )

proof end;

theorem Th57: :: ORDINAL3:57

for b₁, b₂ being Ordinal st one in b₁ & b₂ <> {} & b₂ is_limit_ordinal holds
for b₃ being Ordinal-Sequence st dom b₃ = b₂ & ( for b₄ being Ordinal st b₄ in b₂ holds
b₃ . b₄ = b₄ *^ b₁ ) holds
b₂ *^ b₁ = sup b₃

proof end;

theorem Th58: :: ORDINAL3:58

for b₁, b₂, b₃ being Ordinal holds (b₁ *^ b₂) *^ b₃ = b₁ *^ (b₂ *^ b₃)

proof end;

definition

let c₁, c₂ be Ordinal;
func c₁ -^ c₂ -> Ordinal means :Def6: :: ORDINAL3:def 6
a₁ = a₂ +^ a₃ if a₂ c= a₁
otherwise a₃ = {} ;
existence by Th30;
uniqueness by Th24;
consistency ;
func c₁ div^ c₂ -> Ordinal means :Def7: :: ORDINAL3:def 7
ex b₁ being Ordinal st
( a₁ = (a₃ *^ a₂) +^ b₁ & b₁ in a₂ ) if a₂ <> {}
otherwise a₃ = {} ;
consistency ;
existence by Th55;
uniqueness by Th56;

end;

:: deftheorem Def6 defines -^ ORDINAL3:def 6 :

:: deftheorem Def7 defines div^ ORDINAL3:def 7 :

definition

let c₁, c₂ be Ordinal;
func c₁ mod^ c₂ -> Ordinal equals :: ORDINAL3:def 8
a₁ -^ ((a₁ div^ a₂) *^ a₂);
correctness ;

end;

:: deftheorem Def8 defines mod^ ORDINAL3:def 8 :

theorem Th59: :: ORDINAL3:59

canceled;

theorem Th60: :: ORDINAL3:60

for b₁, b₂ being Ordinal st b₁ in b₂ holds
b₂ = b₁ +^ (b₂ -^ b₁)

proof end;

theorem Th61: :: ORDINAL3:61

canceled;

theorem Th62: :: ORDINAL3:62

canceled;

theorem Th63: :: ORDINAL3:63

canceled;

theorem Th64: :: ORDINAL3:64

canceled;

theorem Th65: :: ORDINAL3:65

for b₁, b₂ being Ordinal holds (b₁ +^ b₂) -^ b₁ = b₂

proof end;

theorem Th66: :: ORDINAL3:66

for b₁, b₂, b₃ being Ordinal st b₁ in b₂ & ( b₃ c= b₁ or b₃ in b₁ ) holds
b₁ -^ b₃ in b₂ -^ b₃

proof end;

theorem Th67: :: ORDINAL3:67

for b₁ being Ordinal holds b₁ -^ b₁ = {}

proof end;

theorem Th68: :: ORDINAL3:68

for b₁, b₂ being Ordinal st b₁ in b₂ holds
( b₂ -^ b₁ <> {} & {} in b₂ -^ b₁ )

proof end;

theorem Th69: :: ORDINAL3:69

for b₁ being Ordinal holds
( b₁ -^ {} = b₁ & {} -^ b₁ = {} )

proof end;

theorem Th70: :: ORDINAL3:70

for b₁, b₂, b₃ being Ordinal holds b₁ -^ (b₂ +^ b₃) = (b₁ -^ b₂) -^ b₃

proof end;

theorem Th71: :: ORDINAL3:71

for b₁, b₂, b₃ being Ordinal st b₁ c= b₂ holds
b₃ -^ b₂ c= b₃ -^ b₁

proof end;

theorem Th72: :: ORDINAL3:72

for b₁, b₂, b₃ being Ordinal st b₁ c= b₂ holds
b₁ -^ b₃ c= b₂ -^ b₃

proof end;

theorem Th73: :: ORDINAL3:73

for b₁, b₂, b₃ being Ordinal st b₁ <> {} & b₂ in b₃ +^ b₁ holds
b₂ -^ b₃ in b₁

proof end;

theorem Th74: :: ORDINAL3:74

for b₁, b₂, b₃ being Ordinal st b₁ +^ b₂ in b₃ holds
b₂ in b₃ -^ b₁

proof end;

theorem Th75: :: ORDINAL3:75

for b₁, b₂ being Ordinal holds b₁ c= b₂ +^ (b₁ -^ b₂)

proof end;

theorem Th76: :: ORDINAL3:76

for b₁, b₂, b₃ being Ordinal holds (b₁ *^ b₂) -^ (b₃ *^ b₂) = (b₁ -^ b₃) *^ b₂

proof end;

theorem Th77: :: ORDINAL3:77

for b₁, b₂ being Ordinal holds (b₁ div^ b₂) *^ b₂ c= b₁

proof end;

theorem Th78: :: ORDINAL3:78

for b₁, b₂ being Ordinal holds b₁ = ((b₁ div^ b₂) *^ b₂) +^ (b₁ mod^ b₂)

proof end;

theorem Th79: :: ORDINAL3:79

for b₁, b₂, b₃, b₄ being Ordinal st b₁ = (b₂ *^ b₃) +^ b₄ & b₄ in b₃ holds
( b₂ = b₁ div^ b₃ & b₄ = b₁ mod^ b₃ )

proof end;

theorem Th80: :: ORDINAL3:80

for b₁, b₂, b₃ being Ordinal st b₁ in b₂ *^ b₃ holds
( b₁ div^ b₃ in b₂ & b₁ mod^ b₃ in b₃ )

proof end;

theorem Th81: :: ORDINAL3:81

for b₁, b₂ being Ordinal st b₁ <> {} holds
(b₂ *^ b₁) div^ b₁ = b₂

proof end;

theorem Th82: :: ORDINAL3:82

for b₁, b₂ being Ordinal holds (b₁ *^ b₂) mod^ b₂ = {}

proof end;

theorem Th83: :: ORDINAL3:83

for b₁ being Ordinal holds
( {} div^ b₁ = {} & {} mod^ b₁ = {} & b₁ mod^ {} = b₁ )

proof end;

theorem Th84: :: ORDINAL3:84

for b₁ being Ordinal holds
( b₁ div^ one = b₁ & b₁ mod^ one = {} )

proof end;