let a, b be Ordinal; :: thesis: 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)))
let n be Nat; :: thesis: ( ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) implies a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b))) )
set c = n *^ (exp (omega,b));
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF (n *^ (exp (omega,b))));
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF (n *^ (exp (omega,b))));
assume A1: ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) ; :: thesis: a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

per cases ( a = 0 or not 0 in n or ( a <> 0 & 0 in n ) ) ;

suppose A2: a = 0 ; :: thesis: a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

hence a (+) (n *^ (exp (omega,b))) = n *^ (exp (omega,b)) by Th82
.= a +^ (n *^ (exp (omega,b))) by A2, ORDINAL2:30 ;
:: thesis: verum

end;

suppose not 0 in n ; :: thesis: a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

then A3: n = 0 by ORDINAL1:16, XBOOLE_1:3;
hence a (+) (n *^ (exp (omega,b))) = a (+) 0 by ORDINAL2:35
.= a by Th82
.= a +^ 0 by ORDINAL2:27
.= a +^ (n *^ (exp (omega,b))) by A3, ORDINAL2:35 ;
:: thesis: verum

end;

suppose A4: ( a <> 0 & 0 in n ) ; :: thesis: a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

then consider A0 being Cantor-normal-form Ordinal-Sequence, a0 being Cantor-component Ordinal such that
A5: CantorNF a = A0 ^ <%a0%> by Th29;
A6: last (CantorNF a) = a0 by A5, AFINSQ_1:92;
consider c being Ordinal, m being Nat such that
A7: ( 0 in Segm m & a0 = m *^ (exp (omega,c)) ) by ORDINAL5:def 9;
( 0 in m & m in omega ) by A7, ORDINAL1:def 12;
then A8: omega -exponent a0 = c by A7, ORDINAL5:58;
n in omega by ORDINAL1:def 12;
then A9: omega -exponent (n *^ (exp (omega,b))) = b by A4, ORDINAL5:58;
then A10: a0 (+) (n *^ (exp (omega,b))) = a0 +^ (n *^ (exp (omega,b))) by A1, A4, A6, A7, A8, Th83;
A11: a (+) (n *^ (exp (omega,b))) = (Sum^ (CantorNF a)) (+) (n *^ (exp (omega,b)))
.= ((Sum^ A0) +^ (Sum^ <%a0%>)) (+) (n *^ (exp (omega,b))) by A5, Th24
.= ((Sum^ A0) (+) (Sum^ <%a0%>)) (+) (n *^ (exp (omega,b))) by A5, Th84
.= (Sum^ A0) (+) ((Sum^ <%a0%>) (+) (n *^ (exp (omega,b)))) by Th81
.= (Sum^ A0) (+) (a0 +^ (n *^ (exp (omega,b)))) by A10, ORDINAL5:53 ;
set A = CantorNF a;

per cases ( b = c or b <> c ) ;

suppose A12: b = c ; :: thesis: a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

set B = A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>;
A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%> is Cantor-normal-form

proof

A13: a0 +^ (n *^ (exp (omega,b))) = (m +^ n) *^ (exp (omega,c)) by A7, A12, ORDINAL3:46
.= (m + n) *^ (exp (omega,c)) by CARD_2:36 ;
A14: 0 < m by A7, NAT_1:44;

A15: now :: thesis: for d being Ordinal st d in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) holds
(A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d is Cantor-component

let d be Ordinal; :: thesis: ( d in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) implies (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁ is Cantor-component )
assume d in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) ; :: thesis: (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁ is Cantor-component

per cases then ( d in dom A0 or ex k being Nat st
( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & d = (len A0) + k ) ) by AFINSQ_1:20;

suppose A16: d in dom A0 ; :: thesis: (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁ is Cantor-component

then A17: ( (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d = A0 . d & A0 . d = (CantorNF a) . d ) by A5, ORDINAL4:def 1;
d in (dom A0) +^ (dom <%a0%>) by A16, ORDINAL3:24, TARSKI:def 3;
then d in dom (CantorNF a) by A5, ORDINAL4:def 1;
hence (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d is Cantor-component by A17, ORDINAL5:def 11; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & d = (len A0) + k ) ; :: thesis: (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁ is Cantor-component

then consider k being Nat such that
A18: ( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & d = (len A0) + k ) ;
k in Segm 1 by A18, AFINSQ_1:33;
then A19: k = 0 by NAT_1:44, NAT_1:14;
(A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d = <%(a0 +^ (n *^ (exp (omega,b))))%> . k by A18, AFINSQ_1:def 3
.= (m + n) *^ (exp (omega,c)) by A13, A19 ;
hence (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d is Cantor-component by A14; :: thesis: verum

end;

end;

end;

now :: thesis: for d, e being Ordinal st d in e & e in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) holds
omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d)

let d, e be Ordinal; :: thesis: ( d in e & e in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) implies omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₂) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁) )
assume A20: ( d in e & e in dom (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) ) ; :: thesis: omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₂) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁)

per cases then ( e in dom A0 or ex k being Nat st
( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & e = (len A0) + k ) ) by AFINSQ_1:20;

suppose A21: e in dom A0 ; :: thesis: omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₂) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁)

then A22: ( (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e = A0 . e & A0 . e = (CantorNF a) . e ) by A5, ORDINAL4:def 1;
e in (dom A0) +^ (dom <%a0%>) by A21, ORDINAL3:24, TARSKI:def 3;
then e in dom (CantorNF a) by A5, ORDINAL4:def 1;
then A23: omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((CantorNF a) . d) by A20, A22, ORDINAL5:def 11;
d in dom A0 by A20, A21, ORDINAL1:10;
then ( (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d = A0 . d & A0 . d = (CantorNF a) . d ) by A5, ORDINAL4:def 1;
hence omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d) by A23; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & e = (len A0) + k ) ; :: thesis: omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₂) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . b₁)

then consider k being Nat such that
A24: ( k in dom <%(a0 +^ (n *^ (exp (omega,b))))%> & e = (len A0) + k ) ;
A25: k in Segm 1 by A24, AFINSQ_1:33;
then A26: k = 0 by NAT_1:44, NAT_1:14;
A27: (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e = <%(a0 +^ (n *^ (exp (omega,b))))%> . k by A24, AFINSQ_1:def 3
.= (m + n) *^ (exp (omega,c)) by A13, A26 ;
0 c< m + n by A14, XBOOLE_1:2, XBOOLE_0:def 8;
then ( 0 in m + n & m + n in omega ) by ORDINAL1:11, ORDINAL1:def 12;
then A28: omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) = c by A27, ORDINAL5:58;
A29: ( (CantorNF a) . d = A0 . d & (A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d = A0 . d ) by A5, A20, A24, A26, ORDINAL4:def 1;
k in dom <%a0%> by A25, AFINSQ_1:33;
then A30: e in dom (CantorNF a) by A5, A24, AFINSQ_1:23;
omega -exponent ((CantorNF a) . e) = omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) by A5, A8, A24, A26, A28, AFINSQ_1:36;
hence omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . e) in omega -exponent ((A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%>) . d) by A20, A29, A30, ORDINAL5:def 11; :: thesis: verum

end;

end;

end;

hence A0 ^ <%(a0 +^ (n *^ (exp (omega,b))))%> is Cantor-normal-form by A15, ORDINAL5:def 11; :: thesis: verum

end;

then (Sum^ A0) (+) (Sum^ <%(a0 +^ (n *^ (exp (omega,b))))%>) = (Sum^ A0) +^ (Sum^ <%(a0 +^ (n *^ (exp (omega,b))))%>) by Th84
.= (Sum^ A0) +^ (a0 +^ (n *^ (exp (omega,b)))) by ORDINAL5:53
.= ((Sum^ A0) +^ a0) +^ (n *^ (exp (omega,b))) by ORDINAL3:30
.= (Sum^ (A0 ^ <%a0%>)) +^ (n *^ (exp (omega,b))) by ORDINAL5:54
.= a +^ (n *^ (exp (omega,b))) by A5 ;
hence a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b))) by A11, ORDINAL5:53; :: thesis: verum

end;

suppose A31: b <> c ; :: thesis: a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))

set B = A0 ^ <%a0,(n *^ (exp (omega,b)))%>;
A0 ^ <%a0,(n *^ (exp (omega,b)))%> is Cantor-normal-form

proof

A32: now :: thesis: for d being Ordinal st d in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) holds
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d is Cantor-component

let d be Ordinal; :: thesis: ( d in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) implies (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁ is Cantor-component )
assume d in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) ; :: thesis: (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁ is Cantor-component

per cases then ( d in dom A0 or ex k being Nat st
( k in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k ) ) by AFINSQ_1:20;

suppose A33: d in dom A0 ; :: thesis: (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁ is Cantor-component

then A34: ( (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = A0 . d & A0 . d = (CantorNF a) . d ) by A5, ORDINAL4:def 1;
d in (dom A0) +^ (dom <%a0%>) by A33, ORDINAL3:24, TARSKI:def 3;
then d in dom (CantorNF a) by A5, ORDINAL4:def 1;
hence (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d is Cantor-component by A34, ORDINAL5:def 11; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k ) ; :: thesis: (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁ is Cantor-component

then consider k being Nat such that
A35: ( k in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k ) ;
k in Segm 2 by AFINSQ_1:38, A35;

per cases then ( k = 0 or k = 1 ) by NAT_1:44, NAT_1:23;

suppose A36: k = 0 ; :: thesis: (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁ is Cantor-component

(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = <%a0,(n *^ (exp (omega,b)))%> . k by A35, AFINSQ_1:def 3
.= a0 by A36 ;
hence (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d is Cantor-component ; :: thesis: verum

end;

suppose A37: k = 1 ; :: thesis: (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁ is Cantor-component

A38: (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = <%a0,(n *^ (exp (omega,b)))%> . k by A35, AFINSQ_1:def 3
.= n *^ (exp (omega,b)) by A37 ;
0 <> n by A4;
hence (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d is Cantor-component by A38; :: thesis: verum

end;

end;

end;

end;

end;

now :: thesis: for d, e being Ordinal st d in e & e in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) holds
omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d)

let d, e be Ordinal; :: thesis: ( d in e & e in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) implies omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁) )
A39: b in c by A1, A4, A6, A8, A31, XBOOLE_0:def 8, ORDINAL1:11;
assume A40: ( d in e & e in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) ) ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

per cases then ( e in dom A0 or ex k2 being Nat st
( k2 in dom <%a0,(n *^ (exp (omega,b)))%> & e = (len A0) + k2 ) ) by AFINSQ_1:20;

suppose A41: e in dom A0 ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

then A42: ( (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e = A0 . e & A0 . e = (CantorNF a) . e ) by A5, ORDINAL4:def 1;
e in (dom A0) +^ (dom <%a0%>) by A41, ORDINAL3:24, TARSKI:def 3;
then e in dom (CantorNF a) by A5, ORDINAL4:def 1;
then A43: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((CantorNF a) . d) by A40, A42, ORDINAL5:def 11;
d in dom A0 by A40, A41, ORDINAL1:10;
then ( (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = A0 . d & A0 . d = (CantorNF a) . d ) by A5, ORDINAL4:def 1;
hence omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) by A43; :: thesis: verum

end;

suppose ex k2 being Nat st
( k2 in dom <%a0,(n *^ (exp (omega,b)))%> & e = (len A0) + k2 ) ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

then consider k2 being Nat such that
A44: ( k2 in dom <%a0,(n *^ (exp (omega,b)))%> & e = (len A0) + k2 ) ;
k2 in Segm 2 by AFINSQ_1:38, A44;
then A45: k2 < 2 by NAT_1:44;
d in dom (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) by A40, ORDINAL1:10;

per cases then ( d in dom A0 or ex k1 being Nat st
( k1 in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k1 ) ) by AFINSQ_1:20;

suppose A46: d in dom A0 ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

then A47: ( (A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = A0 . d & A0 . d = (CantorNF a) . d ) by A5, ORDINAL4:def 1;
0 in Segm 1 by NAT_1:44;
then 0 in dom <%a0%> by AFINSQ_1:33;
then (len A0) + 0 in dom (CantorNF a) by A5, AFINSQ_1:23;
then omega -exponent ((CantorNF a) . (len A0)) in omega -exponent ((CantorNF a) . d) by A46, ORDINAL5:def 11;
then A48: c in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) by A5, A8, A47, AFINSQ_1:36;

per cases ( k2 = 0 or k2 = 1 ) by A45, NAT_1:23;

suppose A49: k2 = 0 ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e = <%a0,(n *^ (exp (omega,b)))%> . k2 by A44, AFINSQ_1:def 3
.= a0 by A49 ;
hence omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) by A8, A48; :: thesis: verum

end;

suppose A50: k2 = 1 ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e = <%a0,(n *^ (exp (omega,b)))%> . k2 by A44, AFINSQ_1:def 3
.= n *^ (exp (omega,b)) by A50 ;
hence omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) by A9, A39, A48, ORDINAL1:10; :: thesis: verum

end;

end;

end;

suppose ex k1 being Nat st
( k1 in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k1 ) ; :: thesis: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₂) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . b₁)

then consider k1 being Nat such that
A51: ( k1 in dom <%a0,(n *^ (exp (omega,b)))%> & d = (len A0) + k1 ) ;
k1 in Segm 2 by AFINSQ_1:38, A51;
then A52: k1 < 2 by NAT_1:44;
A53: ( k1 = 0 & k2 = 1 )

proof

per cases ( ( k1 = 0 & k2 = 0 ) or ( k1 = 0 & k2 = 1 ) or ( k1 = 1 & k2 = 0 ) or ( k1 = 1 & k2 = 1 ) ) by A45, A52, NAT_1:23;

suppose ( k1 = 0 & k2 = 0 ) ; :: thesis: ( k1 = 0 & k2 = 1 )

hence ( k1 = 0 & k2 = 1 ) by A40, A44, A51; :: thesis: verum

end;

suppose ( k1 = 0 & k2 = 1 ) ; :: thesis: ( k1 = 0 & k2 = 1 )

hence ( k1 = 0 & k2 = 1 ) ; :: thesis: verum

end;

suppose A54: ( k1 = 1 & k2 = 0 ) ; :: thesis: ( k1 = 0 & k2 = 1 )

reconsider e = e, d = d as finite Ordinal by A44, A51;
e < d by A44, A51, A54, XREAL_1:8;
then e in Segm d by NAT_1:44;
hence ( k1 = 0 & k2 = 1 ) by A40; :: thesis: verum

end;

suppose ( k1 = 1 & k2 = 1 ) ; :: thesis: ( k1 = 0 & k2 = 1 )

hence ( k1 = 0 & k2 = 1 ) by A40, A44, A51; :: thesis: verum

end;

end;

end;

(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d = <%a0,(n *^ (exp (omega,b)))%> . k1 by A51, AFINSQ_1:def 3
.= a0 by A53 ;
then A55: omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) = c by A8;
(A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e = <%a0,(n *^ (exp (omega,b)))%> . k2 by A44, AFINSQ_1:def 3
.= n *^ (exp (omega,b)) by A53 ;
hence omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . e) in omega -exponent ((A0 ^ <%a0,(n *^ (exp (omega,b)))%>) . d) by A9, A39, A55; :: thesis: verum

end;

end;

end;

end;

end;

hence A0 ^ <%a0,(n *^ (exp (omega,b)))%> is Cantor-normal-form by A32, ORDINAL5:def 11; :: thesis: verum

end;

then (Sum^ A0) (+) (Sum^ <%a0,(n *^ (exp (omega,b)))%>) = (Sum^ A0) +^ (Sum^ <%a0,(n *^ (exp (omega,b)))%>) by Th84
.= (Sum^ A0) +^ (a0 +^ (n *^ (exp (omega,b)))) by Th25
.= ((Sum^ A0) +^ a0) +^ (n *^ (exp (omega,b))) by ORDINAL3:30
.= (Sum^ (A0 ^ <%a0%>)) +^ (n *^ (exp (omega,b))) by ORDINAL5:54
.= a +^ (n *^ (exp (omega,b))) by A5 ;
hence a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b))) by A11, Th25; :: thesis: verum

end;

end;

end;

end;