:: by Sebastian Koch

::

:: Received May 27, 2019

:: Copyright (c) 2019-2021 Association of Mizar Users

:: into ORDINAL1 ?

:: into ORDINAL2 ?

registration
end;

Lm1: succ 0 = 1

;

Lm2: succ (succ 0) = 2

;

:: into ORDINAL2 ?

:: into ORDINAL2 ?

:: into ORDINAL2 ?

:: into ORDINAL4 ?

:: a |^|^ 2 = exp(a, a) is ORDINAL5:18

:: into ORDINAL5 ?

:: into ORDINAL5 ?

Th9: for A, B being Sequence holds rng (A ^ B) = (rng A) \/ (rng B)

by ORDINAL4:2;

:: into ORDINAL4 ?

theorem Th10: :: ORDINAL7:7

for A, B being Sequence st A ^ B is Ordinal-yielding holds

( A is Ordinal-yielding & B is Ordinal-yielding )

( A is Ordinal-yielding & B is Ordinal-yielding )

proof end;

Th13: for D being set

for p being FinSequence of D

for n being Nat holds

( n + 1 in dom p iff n in dom (FS2XFS p) )

by AFINSQ_1:94;

Th15: for D being set

for p being FinSequence of D holds rng p = rng (FS2XFS p)

by AFINSQ_1:96;

Th19: for D being set

for p being one-to-one XFinSequence of D

for n being Nat holds rng (p | n) misses rng (p /^ n)

by AFINSQ_2:87;

:: into ORDINAL5 ?

:: corrolary from theorem above

:: corrolary from theorem above

:: into ORDINAL5 ?

:: into ORDINAL5 ?

:: into ORDINAL5 ?

registration

for b_{1} being Ordinal-Sequence st b_{1} is decreasing holds

b_{1} is one-to-one
end;

cluster Relation-like Function-like Sequence-like Ordinal-yielding decreasing -> one-to-one for set ;

coherence for b

b

proof end;

:: into ORDINAL5 ?

registration
end;

:: into ORDINAL5 ?

registration
end;

:: into ORDINAL5 ?

registration
end;

:: into ORDINAL5 ?

:: into ORDINAL5 ?

:: into ORDINAL5 ?

registration

let A be non-empty non empty finite Ordinal-Sequence;

coherence

not Sum^ A is empty

coherence

not Sum^ (A ^ B) is empty

not Sum^ (B ^ A) is empty

end;
coherence

not Sum^ A is empty

proof end;

let B be finite Ordinal-Sequence;coherence

not Sum^ (A ^ B) is empty

proof end;

coherence not Sum^ (B ^ A) is empty

proof end;

:: into ORDINAL5 ?

Lm5: for n being Nat holds succ n = n + 1

proof end;

:: into ORDINAL5 ?

:: into ORDINAL5 ?

theorem Th28: :: ORDINAL7:15

for A, B being finite Ordinal-Sequence st dom A c= dom B & ( for a being object st a in dom A holds

A . a c= B . a ) holds

Sum^ A c= Sum^ B

A . a c= B . a ) holds

Sum^ A c= Sum^ B

proof end;

:: into ORDINAL5 ?

:: the mirror theorem of ORDINAL5:67

:: the mirror theorem of ORDINAL5:67

theorem Th29: :: ORDINAL7:16

for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds

ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%>

ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%>

proof end;

:: into ORDINAL5 ?

registration

let A be Cantor-normal-form Ordinal-Sequence;

let n be Nat;

coherence

A | n is Cantor-normal-form

end;
let n be Nat;

coherence

A | n is Cantor-normal-form

proof end;

:: into ORDINAL5 or AFINSQ_2 ?

registration

let A be Cantor-normal-form Ordinal-Sequence;

let n be Nat;

coherence

A /^ n is Cantor-normal-form

end;
let n be Nat;

coherence

A /^ n is Cantor-normal-form

proof end;

registration

coherence

for b_{1} being Sequence st b_{1} is natural-valued holds

b_{1} is Ordinal-yielding

end;
for b

b

proof end;

registration

coherence

for b_{1} being Nat st b_{1} is limit_ordinal holds

b_{1} is zero
;

existence

not for b_{1} being Ordinal holds b_{1} is limit_ordinal

end;
for b

b

existence

not for b

proof end;

registration

let n, m be Nat;

correctness

compatibility

n \/ m = max (n,m);

compatibility

n /\ m = min (n,m);

end;
correctness

compatibility

n \/ m = max (n,m);

proof end;

correctness compatibility

n /\ m = min (n,m);

proof end;

:: absorption law of ordinal numbers

theorem Th31: :: ORDINAL7:18

for A being non empty Cantor-normal-form Ordinal-Sequence

for a being object st a in dom A holds

omega -exponent (last A) c= omega -exponent (A . a)

for a being object st a in dom A holds

omega -exponent (last A) c= omega -exponent (A . a)

proof end;

theorem Th32: :: ORDINAL7:19

for A being non empty Cantor-normal-form Ordinal-Sequence

for a being object st a in dom A holds

omega -exponent (A . a) c= omega -exponent (A . 0)

for a being object st a in dom A holds

omega -exponent (A . a) c= omega -exponent (A . 0)

proof end;

:: this implies ORDINAL5:68

theorem Th33: :: ORDINAL7:20

for A, B being non empty Cantor-normal-form Ordinal-Sequence st omega -exponent (B . 0) in omega -exponent (last A) holds

A ^ B is Cantor-normal-form

A ^ B is Cantor-normal-form

proof end;

Lm6: for A being decreasing Ordinal-Sequence

for n being Nat st len A = n + 1 holds

rng (A | n) = (rng A) \ {(A . n)}

proof end;

Lm7: for A, B being decreasing Ordinal-Sequence

for n being Nat st len A = n + 1 & rng A = rng B holds

A . n = B . n

proof end;

registration

let a be Ordinal;

coherence

exp (omega,a) is Cantor-component

coherence

n *^ (exp (omega,a)) is Cantor-component

end;
coherence

exp (omega,a) is Cantor-component

proof end;

let n be non zero Nat;coherence

n *^ (exp (omega,a)) is Cantor-component

proof end;

registration
end;

registration
end;

theorem Th35: :: ORDINAL7:22

for c, d being Cantor-component Ordinal st omega -exponent d in omega -exponent c holds

<%c,d%> is Cantor-normal-form

<%c,d%> is Cantor-normal-form

proof end;

Lm8: for a being non empty Ordinal

for n, m being non zero Nat holds <%(n *^ (exp (omega,a))),m%> is Cantor-normal-form

proof end;

registration

let a be non empty Ordinal;

let m be non zero Nat;

coherence

<%(exp (omega,a)),m%> is Cantor-normal-form

coherence

<%(n *^ (exp (omega,a))),m%> is Cantor-normal-form by Lm8;

end;
let m be non zero Nat;

coherence

<%(exp (omega,a)),m%> is Cantor-normal-form

proof end;

let n be non zero Nat;coherence

<%(n *^ (exp (omega,a))),m%> is Cantor-normal-form by Lm8;

theorem :: ORDINAL7:23

for c, d, e being Cantor-component Ordinal st omega -exponent d in omega -exponent c & omega -exponent e in omega -exponent d holds

<%c,d,e%> is Cantor-normal-form

<%c,d,e%> is Cantor-normal-form

proof end;

theorem Th37: :: ORDINAL7:24

for A being non empty Cantor-normal-form Ordinal-Sequence

for b being Ordinal

for n being non zero Nat st b in omega -exponent (last A) holds

A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form

for b being Ordinal

for n being non zero Nat st b in omega -exponent (last A) holds

A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form

proof end;

theorem :: ORDINAL7:25

for A being non empty Cantor-normal-form Ordinal-Sequence

for b being Ordinal

for n being non zero Nat st omega -exponent (last A) <> 0 holds

A ^ <%n%> is Cantor-normal-form

for b being Ordinal

for n being non zero Nat st omega -exponent (last A) <> 0 holds

A ^ <%n%> is Cantor-normal-form

proof end;

:: variant of ORDINAL5:68

theorem Th39: :: ORDINAL7:26

for A being non empty Cantor-normal-form Ordinal-Sequence

for b being Ordinal

for n being non zero Nat st omega -exponent (A . 0) in b holds

<%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form

for b being Ordinal

for n being non zero Nat st omega -exponent (A . 0) in b holds

<%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form

proof end;

:: closure of ordinal addition

theorem Th40: :: ORDINAL7:27

for a1, a2, b being Ordinal st a1 in exp (omega,b) & a2 in exp (omega,b) holds

a1 +^ a2 in exp (omega,b)

a1 +^ a2 in exp (omega,b)

proof end;

theorem Th41: :: ORDINAL7:28

for A being finite Ordinal-Sequence

for b being Ordinal st ( for a being Ordinal st a in dom A holds

A . a in exp (omega,b) ) holds

Sum^ A in exp (omega,b)

for b being Ordinal st ( for a being Ordinal st a in dom A holds

A . a in exp (omega,b) ) holds

Sum^ A in exp (omega,b)

proof end;

:: variant of ORDINAL5:7

theorem Th43: :: ORDINAL7:30

for A being finite Ordinal-Sequence

for a being Ordinal st <%a%> ^ A is Cantor-normal-form holds

Sum^ A in exp (omega,(omega -exponent a))

for a being Ordinal st <%a%> ^ A is Cantor-normal-form holds

Sum^ A in exp (omega,(omega -exponent a))

proof end;

theorem Th44: :: ORDINAL7:31

for A being Cantor-normal-form Ordinal-Sequence holds omega -exponent (Sum^ A) = omega -exponent (A . 0)

proof end;

definition

let A be Ordinal-Sequence;

let b be Ordinal;

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom A & ( for a being object st a in dom A holds

b_{1} . a = b -exponent (A . a) ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom A & ( for a being object st a in dom A holds

b_{1} . a = b -exponent (A . a) ) & dom b_{2} = dom A & ( for a being object st a in dom A holds

b_{2} . a = b -exponent (A . a) ) holds

b_{1} = b_{2}

end;
let b be Ordinal;

func b -exponent A -> Ordinal-Sequence means :Def1: :: ORDINAL7:def 1

( dom it = dom A & ( for a being object st a in dom A holds

it . a = b -exponent (A . a) ) );

existence ( dom it = dom A & ( for a being object st a in dom A holds

it . a = b -exponent (A . a) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines -exponent ORDINAL7:def 1 :

for A being Ordinal-Sequence

for b being Ordinal

for b_{3} being Ordinal-Sequence holds

( b_{3} = b -exponent A iff ( dom b_{3} = dom A & ( for a being object st a in dom A holds

b_{3} . a = b -exponent (A . a) ) ) );

for A being Ordinal-Sequence

for b being Ordinal

for b

( b

b

registration
end;

registration

let A be non empty Ordinal-Sequence;

let b be Ordinal;

coherence

not b -exponent A is empty

end;
let b be Ordinal;

coherence

not b -exponent A is empty

proof end;

registration
end;

registration

let A be infinite Ordinal-Sequence;

let b be Ordinal;

coherence

not b -exponent A is finite

end;
let b be Ordinal;

coherence

not b -exponent A is finite

proof end;

theorem Th47: :: ORDINAL7:34

for A, B being Ordinal-Sequence

for b being Ordinal holds b -exponent (A ^ B) = (b -exponent A) ^ (b -exponent B)

for b being Ordinal holds b -exponent (A ^ B) = (b -exponent A) ^ (b -exponent B)

proof end;

theorem Th49: :: ORDINAL7:36

for A being finite Ordinal-Sequence

for b being Ordinal

for n being Nat holds b -exponent (A /^ n) = (b -exponent A) /^ n

for b being Ordinal

for n being Nat holds b -exponent (A /^ n) = (b -exponent A) /^ n

proof end;

registration
end;

theorem :: ORDINAL7:37

for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds

rng (omega -exponent A) misses rng (omega -exponent B)

rng (omega -exponent A) misses rng (omega -exponent B)

proof end;

theorem Th51: :: ORDINAL7:38

for A being Cantor-normal-form Ordinal-Sequence holds

( 0 in rng (omega -exponent A) iff ( A <> {} & omega -exponent (last A) = 0 ) )

( 0 in rng (omega -exponent A) iff ( A <> {} & omega -exponent (last A) = 0 ) )

proof end;

:: deftheorem defines -leading_coeff ORDINAL7:def 2 :

for a, b being Ordinal holds b -leading_coeff a = a div^ (exp (b,(b -exponent a)));

for a, b being Ordinal holds b -leading_coeff a = a div^ (exp (b,(b -exponent a)));

:: This is the undefined case. One could have set the value simply to 0

:: in case that b = 0 just as well.

:: in case that b = 0 just as well.

:: this means that a = a *^ exp(1,0)

:: this means that 0 = 0 *^ exp(b,0)

:: this means that a = a *^ exp(b,0)

:: this means that 1 = 1 *^ exp(b,0)

registration

let c be Cantor-component Ordinal;

coherence

( omega -leading_coeff c is natural & not omega -leading_coeff c is empty )

end;
coherence

( omega -leading_coeff c is natural & not omega -leading_coeff c is empty )

proof end;

theorem Th59: :: ORDINAL7:46

for c being Cantor-component Ordinal holds c = (omega -leading_coeff c) *^ (exp (omega,(omega -exponent c)))

proof end;

definition

let A be Ordinal-Sequence;

let b be Ordinal;

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom A & ( for a being object st a in dom A holds

b_{1} . a = b -leading_coeff (A . a) ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom A & ( for a being object st a in dom A holds

b_{1} . a = b -leading_coeff (A . a) ) & dom b_{2} = dom A & ( for a being object st a in dom A holds

b_{2} . a = b -leading_coeff (A . a) ) holds

b_{1} = b_{2}

end;
let b be Ordinal;

func b -leading_coeff A -> Ordinal-Sequence means :Def3: :: ORDINAL7:def 3

( dom it = dom A & ( for a being object st a in dom A holds

it . a = b -leading_coeff (A . a) ) );

existence ( dom it = dom A & ( for a being object st a in dom A holds

it . a = b -leading_coeff (A . a) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines -leading_coeff ORDINAL7:def 3 :

for A being Ordinal-Sequence

for b being Ordinal

for b_{3} being Ordinal-Sequence holds

( b_{3} = b -leading_coeff A iff ( dom b_{3} = dom A & ( for a being object st a in dom A holds

b_{3} . a = b -leading_coeff (A . a) ) ) );

for A being Ordinal-Sequence

for b being Ordinal

for b

( b

b

registration
end;

registration

let A be non empty Ordinal-Sequence;

let b be Ordinal;

coherence

not b -leading_coeff A is empty

end;
let b be Ordinal;

coherence

not b -leading_coeff A is empty

proof end;

registration

let A be finite Ordinal-Sequence;

let b be Ordinal;

coherence

b -leading_coeff A is finite

end;
let b be Ordinal;

coherence

b -leading_coeff A is finite

proof end;

registration

let A be infinite Ordinal-Sequence;

let b be Ordinal;

coherence

not b -leading_coeff A is finite

end;
let b be Ordinal;

coherence

not b -leading_coeff A is finite

proof end;

theorem :: ORDINAL7:48

for A, B being Ordinal-Sequence

for b being Ordinal holds b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)

for b being Ordinal holds b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)

proof end;

theorem :: ORDINAL7:49

for A being Ordinal-Sequence

for b, c being Ordinal holds b -leading_coeff (A | c) = (b -leading_coeff A) | c

for b, c being Ordinal holds b -leading_coeff (A | c) = (b -leading_coeff A) | c

proof end;

theorem :: ORDINAL7:50

for A being finite Ordinal-Sequence

for b being Ordinal

for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n

for b being Ordinal

for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n

proof end;

registration

let A be Cantor-normal-form Ordinal-Sequence;

let a be object ;

coherence

(omega -leading_coeff A) . a is natural

end;
let a be object ;

coherence

(omega -leading_coeff A) . a is natural

proof end;

registration

let A be Cantor-normal-form Ordinal-Sequence;

coherence

( omega -leading_coeff A is natural-valued & omega -leading_coeff A is non-empty )

end;
coherence

( omega -leading_coeff A is natural-valued & omega -leading_coeff A is non-empty )

proof end;

theorem Th64: :: ORDINAL7:51

for A being Cantor-normal-form Ordinal-Sequence

for a being object st a in dom A holds

A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))

for a being object st a in dom A holds

A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))

proof end;

theorem Th65: :: ORDINAL7:52

for A being Cantor-normal-form Ordinal-Sequence

for a being object st a in dom A holds

A . a = ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a)))

for a being object st a in dom A holds

A . a = ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a)))

proof end;

theorem Th66: :: ORDINAL7:53

for A being decreasing Ordinal-Sequence

for B being non-empty natural-valued Ordinal-Sequence st dom A = dom B holds

ex C being Cantor-normal-form Ordinal-Sequence st

( omega -exponent C = A & omega -leading_coeff C = B )

for B being non-empty natural-valued Ordinal-Sequence st dom A = dom B holds

ex C being Cantor-normal-form Ordinal-Sequence st

( omega -exponent C = A & omega -leading_coeff C = B )

proof end;

theorem Th67: :: ORDINAL7:54

for A, B being Cantor-normal-form Ordinal-Sequence st omega -exponent A = omega -exponent B & omega -leading_coeff A = omega -leading_coeff B holds

A = B

A = B

proof end;

definition

let a be Ordinal;

existence

ex b_{1} being Cantor-normal-form Ordinal-Sequence st Sum^ b_{1} = a
by ORDINAL5:69;

uniqueness

for b_{1}, b_{2} being Cantor-normal-form Ordinal-Sequence st Sum^ b_{1} = a & Sum^ b_{2} = a holds

b_{1} = b_{2}
by Th45;

end;
existence

ex b

uniqueness

for b

b

:: deftheorem Def4 defines CantorNF ORDINAL7:def 4 :

for a being Ordinal

for b_{2} being Cantor-normal-form Ordinal-Sequence holds

( b_{2} = CantorNF a iff Sum^ b_{2} = a );

for a being Ordinal

for b

( b

registration

let A be Cantor-normal-form Ordinal-Sequence;

correctness

reducibility

CantorNF (Sum^ A) = A;

by Def4;

end;
correctness

reducibility

CantorNF (Sum^ A) = A;

by Def4;

theorem Th69: :: ORDINAL7:56

for a being Ordinal

for n being non zero Nat holds CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%>

for n being non zero Nat holds CantorNF (n *^ (exp (omega,a))) = <%(n *^ (exp (omega,a)))%>

proof end;

theorem :: ORDINAL7:59

for a being non empty Ordinal

for n, m being non zero Nat holds CantorNF ((n *^ (exp (omega,a))) +^ m) = <%(n *^ (exp (omega,a))),m%>

for n, m being non zero Nat holds CantorNF ((n *^ (exp (omega,a))) +^ m) = <%(n *^ (exp (omega,a))),m%>

proof end;

theorem Th73: :: ORDINAL7:60

for a being non empty Ordinal

for b being Ordinal

for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds

CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>

for b being Ordinal

for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds

CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>

proof end;

theorem :: ORDINAL7:61

for a being non empty Ordinal

for n being non zero Nat st omega -exponent (last (CantorNF a)) <> 0 holds

CantorNF (a +^ n) = (CantorNF a) ^ <%n%>

for n being non zero Nat st omega -exponent (last (CantorNF a)) <> 0 holds

CantorNF (a +^ n) = (CantorNF a) ^ <%n%>

proof end;

theorem :: ORDINAL7:62

for a being non empty Ordinal

for b being Ordinal

for n being non zero Nat st omega -exponent ((CantorNF a) . 0) in b holds

CantorNF ((n *^ (exp (omega,b))) +^ a) = <%(n *^ (exp (omega,b)))%> ^ (CantorNF a)

for b being Ordinal

for n being non zero Nat st omega -exponent ((CantorNF a) . 0) in b holds

CantorNF ((n *^ (exp (omega,b))) +^ a) = <%(n *^ (exp (omega,b)))%> ^ (CantorNF a)

proof end;

definition

let a, b be Ordinal;

ex b_{1} being Ordinal ex C being Cantor-normal-form Ordinal-Sequence st

( b_{1} = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) )

for b_{1}, b_{2} being Ordinal st ex C being Cantor-normal-form Ordinal-Sequence st

( b_{1} = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) & ex C being Cantor-normal-form Ordinal-Sequence st

( b_{2} = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds

b_{1} = b_{2}

for b_{1}, a, b being Ordinal st ex C being Cantor-normal-form Ordinal-Sequence st

( b_{1} = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds

ex C being Cantor-normal-form Ordinal-Sequence st

( b_{1} = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF a))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) ) ) ) )

end;
func a (+) b -> Ordinal means :Def5: :: ORDINAL7:def 5

ex C being Cantor-normal-form Ordinal-Sequence st

( it = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) );

existence ex C being Cantor-normal-form Ordinal-Sequence st

( it = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) );

ex b

( b

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) )

proof end;

uniqueness for b

( b

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) & ex C being Cantor-normal-form Ordinal-Sequence st

( b

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds

b

proof end;

commutativity for b

( b

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) holds

ex C being Cantor-normal-form Ordinal-Sequence st

( b

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) ) ) ) )

proof end;

:: deftheorem Def5 defines (+) ORDINAL7:def 5 :

for a, b, b_{3} being Ordinal holds

( b_{3} = a (+) b iff ex C being Cantor-normal-form Ordinal-Sequence st

( b_{3} = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) );

for a, b, b

( b

( b

( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) );

theorem Th76: :: ORDINAL7:63

for a, b being Ordinal holds rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))

proof end;

theorem Th78: :: ORDINAL7:65

for a, b being Ordinal

for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) holds

omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))

for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) holds

omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))

proof end;

theorem Th79: :: ORDINAL7:66

for a, b being Ordinal

for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) holds

omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) by Th78;

for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) holds

omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) by Th78;

theorem Th80: :: ORDINAL7:67

for a, b being Ordinal

for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) holds

omega -leading_coeff ((CantorNF (a (+) b)) . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))))

for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) holds

omega -leading_coeff ((CantorNF (a (+) b)) . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))))

proof end;

theorem Th83: :: ORDINAL7:70

for a, b being Ordinal

for n being Nat st omega -exponent a c= b holds

(n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a

for n being Nat st omega -exponent a c= b holds

(n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a

proof end;

theorem Th84: :: ORDINAL7:71

for A, B being finite Ordinal-Sequence st A ^ B is Cantor-normal-form holds

(Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)

(Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)

proof end;

theorem Th85: :: ORDINAL7:72

for a, b being Ordinal st ( a <> 0 implies omega -exponent b in omega -exponent (last (CantorNF a)) ) holds

a (+) b = a +^ b

a (+) b = a +^ b

proof end;

theorem Th86: :: ORDINAL7:73

for a, b being Ordinal

for n being Nat st ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) holds

a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

for n being Nat st ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) holds

a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

proof end;

theorem :: ORDINAL7:74

for a being Ordinal

for n, m being Nat holds (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))

for n, m being Nat holds (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))

proof end;

registration
end;

registration
end;

registration

let a be Ordinal;

let b be non limit_ordinal Ordinal;

coherence

not a (+) b is limit_ordinal

end;
let b be non limit_ordinal Ordinal;

coherence

not a (+) b is limit_ordinal

proof end;

theorem :: ORDINAL7:80

for a, b being Ordinal

for n being non zero Nat st n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) holds

(CantorNF a) . 0 = n *^ (exp (omega,b))

for n being non zero Nat st n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) holds

(CantorNF a) . 0 = n *^ (exp (omega,b))

proof end;

theorem :: ORDINAL7:81

for a, b being Ordinal st rng (omega -exponent (CantorNF a)) = rng (omega -exponent (CantorNF b)) holds

for c being Ordinal st c in dom (CantorNF a) holds

(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)

for c being Ordinal st c in dom (CantorNF a) holds

(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)

proof end;

theorem Th95: :: ORDINAL7:82

for a, b being Ordinal holds

( ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 ) )

( ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 ) )

proof end;

theorem :: ORDINAL7:83

for a, b being Ordinal holds

( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )

( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )

proof end;

theorem Th97: :: ORDINAL7:84

for a, b being Ordinal

for x being object holds (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x

for x being object holds (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x

proof end;

:: closure of natural addition

Lm9: for a being Ordinal

for n being Nat holds (n *^ (exp (omega,a))) +^ (exp (omega,a)) = (n *^ (exp (omega,a))) (+) (exp (omega,a))

proof end;

scheme :: ORDINAL7:sch 1

OrdinalCNFIndA{ P_{1}[ non empty Ordinal] } :

provided

OrdinalCNFIndA{ P

provided

A1:
for a being Ordinal

for n being non zero Nat holds P_{1}[n *^ (exp (omega,a))]
and

A2: for a being Ordinal

for b being non empty Ordinal

for n being non zero Nat st P_{1}[b] & not a in rng (omega -exponent (CantorNF b)) holds

P_{1}[b (+) (n *^ (exp (omega,a)))]

for n being non zero Nat holds P

A2: for a being Ordinal

for b being non empty Ordinal

for n being non zero Nat st P

P

proof end;

scheme :: ORDINAL7:sch 2

OrdinalCNFIndB{ P_{1}[ non empty Ordinal] } :

provided

OrdinalCNFIndB{ P

provided

A1:
for a being Ordinal holds P_{1}[ exp (omega,a)]
and

A2: for a being Ordinal

for n being non zero Nat st P_{1}[n *^ (exp (omega,a))] holds

P_{1}[(n + 1) *^ (exp (omega,a))]
and

A3: for a being Ordinal

for b being non empty Ordinal

for n being non zero Nat st P_{1}[b] & not a in rng (omega -exponent (CantorNF b)) holds

P_{1}[b (+) (n *^ (exp (omega,a)))]

A2: for a being Ordinal

for n being non zero Nat st P

P

A3: for a being Ordinal

for b being non empty Ordinal

for n being non zero Nat st P

P

proof end;

theorem Th102: :: ORDINAL7:89

for a, b being Ordinal st omega -exponent a in omega -exponent b holds

a in exp (omega,(omega -exponent b))

a in exp (omega,(omega -exponent b))

proof end;

theorem Th103: :: ORDINAL7:90

for a, b being non empty Ordinal holds

( omega *^ a c= b iff omega -exponent a in omega -exponent b )

( omega *^ a c= b iff omega -exponent a in omega -exponent b )

proof end;

:: cancelling rule for natural addition

Lm10: for A being Cantor-normal-form Ordinal-Sequence holds omega -exponent A is XFinSequence of sup (omega -exponent A)

proof end;

Lm11: for a being non empty Ordinal

for b, c being Ordinal st b in c & (CantorNF b) . 0 <> (CantorNF c) . 0 holds

a (+) b in a (+) c

proof end;

:: monotonicity of natural addition