let a, b be Ordinal; :: thesis: for n being Nat st omega -exponent a c= b holds
(n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a
let n be Nat; :: thesis: ( omega -exponent a c= b implies (n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a )
set E1 = omega -exponent (CantorNF (n *^ (exp (omega,b))));
set E2 = omega -exponent (CantorNF a);
set L1 = omega -leading_coeff (CantorNF (n *^ (exp (omega,b))));
set L2 = omega -leading_coeff (CantorNF a);
assume omega -exponent a c= b ; :: thesis: (n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a
then omega -exponent (Sum^ (CantorNF a)) c= b ;
then A1: omega -exponent ((CantorNF a) . 0) c= b by Th44;
A2: (omega -exponent (CantorNF a)) . 0 c= b

proof

per cases ( 0 in dom (CantorNF a) or not 0 in dom (CantorNF a) ) ;

suppose 0 in dom (CantorNF a) ; :: thesis: (omega -exponent (CantorNF a)) . 0 c= b

hence (omega -exponent (CantorNF a)) . 0 c= b by A1, Def1; :: thesis: verum

end;

suppose not 0 in dom (CantorNF a) ; :: thesis: (omega -exponent (CantorNF a)) . 0 c= b

then not 0 in dom (omega -exponent (CantorNF a)) by Def1;
then (omega -exponent (CantorNF a)) . 0 = {} by FUNCT_1:def 2;
hence (omega -exponent (CantorNF a)) . 0 c= b ; :: thesis: verum

end;

end;

end;

consider C being Cantor-normal-form Ordinal-Sequence such that
A3: (n *^ (exp (omega,b))) (+) a = Sum^ C and
A4: rng (omega -exponent C) = (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) \/ (rng (omega -exponent (CantorNF a))) and
A5: for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . (((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF (n *^ (exp (omega,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 (n *^ (exp (omega,b)))))) /\ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . (((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) ) ) by Def5;

per cases ( a = 0 or n is zero or ( not n is zero & a <> 0 & (omega -exponent (CantorNF a)) . 0 = b ) or ( not n is zero & a <> 0 & (omega -exponent (CantorNF a)) . 0 <> b ) ) ;

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

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

end;

suppose A7: n is zero ; :: thesis: (n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a

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

end;

suppose A8: ( not n is zero & a <> 0 & (omega -exponent (CantorNF a)) . 0 = b ) ; :: thesis: (n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a

then consider a0 being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A9: CantorNF a = <%a0%> ^ A0 by ORDINAL5:67;
0 c< n by A8, XBOOLE_1:2, XBOOLE_0:def 8;
then A10: ( 0 in n & n in omega ) by ORDINAL1:11, ORDINAL1:def 12;
A11: omega -exponent (CantorNF (n *^ (exp (omega,b)))) = omega -exponent <%(n *^ (exp (omega,b)))%> by A8, Th69
.= <%(omega -exponent (n *^ (exp (omega,b))))%> by Th46
.= <%b%> by A10, ORDINAL5:58 ;
then A12: rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) = {b} by AFINSQ_1:33;
0 c< dom (CantorNF a) by A8, XBOOLE_1:2, XBOOLE_0:def 8;
then A13: 0 in dom (CantorNF a) by ORDINAL1:11;
then A14: 0 in dom (omega -exponent (CantorNF a)) by Def1;
then rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) c= rng (omega -exponent (CantorNF a)) by A8, A12, FUNCT_1:3, ZFMISC_1:31;
then A15: omega -exponent C = omega -exponent (CantorNF a) by A4, Th34, XBOOLE_1:12;
A16: dom C = card (dom (omega -exponent C)) by Def1
.= len (<%a0%> ^ A0) by A15, A9, Def1
.= (len <%a0%>) + (len A0) by AFINSQ_1:17
.= 1 + (len A0) by AFINSQ_1:34
.= (len <%((n *^ (exp (omega,b))) +^ a0)%>) + (len A0) by AFINSQ_1:34
.= dom (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) by AFINSQ_1:17 ;
for x being object st x in dom C holds
C . x = (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x

proof

let x be object ; :: thesis: ( x in dom C implies C . x = (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x )
assume A17: x in dom C ; :: thesis: C . x = (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x
A18: dom C = dom (omega -exponent (CantorNF a)) by Def1, A15;

per cases ( omega -exponent (C . x) = b or omega -exponent (C . x) <> b ) ;

suppose A19: omega -exponent (C . x) = b ; :: thesis: C . x = (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x

then b = (omega -exponent (CantorNF a)) . x by A15, A17, Def1;
then A20: x = 0 by A8, A14, A17, A18, FUNCT_1:def 4;
A21: omega -exponent (C . x) in rng (omega -exponent (CantorNF a)) by A8, A14, A19, FUNCT_1:3;
omega -exponent (C . x) in rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by A12, A19, TARSKI:def 1;
then A22: omega -exponent (C . x) in (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) /\ (rng (omega -exponent (CantorNF a))) by A21, XBOOLE_0:def 4;
A23: (omega -exponent (CantorNF (n *^ (exp (omega,b))))) . 0 = b by A11;
dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) = 1 by A11, AFINSQ_1:34;
then A24: 0 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by CARD_1:49, TARSKI:def 1;
A25: omega -leading_coeff (C . x) = ((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . (((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ") . (omega -exponent (C . x)))) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . b)) by A5, A17, A19, A22
.= ((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0) + ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . b)) by A19, A23, A24, FUNCT_1:34
.= ((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0) + ((omega -leading_coeff (CantorNF a)) . 0) by A8, A14, FUNCT_1:34
.= ((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0) +^ ((omega -leading_coeff (CantorNF a)) . 0) by CARD_2:36 ;
A26: (omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0 = (omega -leading_coeff <%(n *^ (exp (omega,b)))%>) . 0 by A8, Th69
.= <%(omega -leading_coeff (n *^ (exp (omega,b))))%> . 0 by Th60
.= n by Th57, ORDINAL1:def 12 ;
thus C . x = (((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0) +^ ((omega -leading_coeff (CantorNF a)) . 0)) *^ (exp (omega,(omega -exponent (C . x)))) by A17, A25, Th64
.= (((omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0) *^ (exp (omega,b))) +^ (((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0)))) by A8, A19, ORDINAL3:46
.= (n *^ (exp (omega,b))) +^ ((CantorNF a) . 0) by A13, A26, Th65
.= (n *^ (exp (omega,b))) +^ a0 by A9, AFINSQ_1:35
.= (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x by A20, AFINSQ_1:35 ; :: thesis: verum

end;

suppose A27: omega -exponent (C . x) <> b ; :: thesis: C . x = (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x

then A28: not omega -exponent (C . x) in rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by A12, TARSKI:def 1;
x in dom (omega -exponent C) by A17, Def1;
then (omega -exponent C) . x in rng (omega -exponent C) by FUNCT_1:3;
then omega -exponent (C . x) in (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) \/ (rng (omega -exponent (CantorNF a))) by A4, A17, Def1;
then ( omega -exponent (C . x) in rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) or omega -exponent (C . x) in rng (omega -exponent (CantorNF a)) ) by XBOOLE_0:def 3;
then omega -exponent (C . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) by A28, XBOOLE_0:def 5;
then A29: omega -leading_coeff (C . x) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . x))) by A5, A17
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent C) . x)) by A17, Def1
.= (omega -leading_coeff (CantorNF a)) . x by A15, A17, A18, FUNCT_1:34 ;
(omega -exponent C) . x <> b by A17, A27, Def1;
then not x in 1 by A8, A15, CARD_1:49, TARSKI:def 1;
then not x in len <%((n *^ (exp (omega,b))) +^ a0)%> by AFINSQ_1:34;
then consider m being Nat such that
A30: ( m in dom A0 & x = (len <%((n *^ (exp (omega,b))) +^ a0)%>) + m ) by A16, A17, AFINSQ_1:20;
A31: x = 1 + m by A30, AFINSQ_1:34
.= (len <%a0%>) + m by AFINSQ_1:34 ;
A32: x in dom (CantorNF a) by A17, A18, Def1;
thus C . x = ((omega -leading_coeff (CantorNF a)) . x) *^ (exp (omega,(omega -exponent (C . x)))) by A17, A29, Th64
.= ((omega -leading_coeff (CantorNF a)) . x) *^ (exp (omega,((omega -exponent C) . x))) by A17, Def1
.= (CantorNF a) . x by A15, A32, Th65
.= A0 . m by A9, A30, A31, AFINSQ_1:def 3
.= (<%((n *^ (exp (omega,b))) +^ a0)%> ^ A0) . x by A30, AFINSQ_1:def 3 ; :: thesis: verum

end;

end;

end;

then C = <%((n *^ (exp (omega,b))) +^ a0)%> ^ A0 by A16, FUNCT_1:2;
hence (n *^ (exp (omega,b))) (+) a = ((n *^ (exp (omega,b))) +^ a0) +^ (Sum^ A0) by A3, ORDINAL5:55
.= (n *^ (exp (omega,b))) +^ (a0 +^ (Sum^ A0)) by ORDINAL3:30
.= (n *^ (exp (omega,b))) +^ (Sum^ (<%a0%> ^ A0)) by ORDINAL5:55
.= (n *^ (exp (omega,b))) +^ a by A9 ;
:: thesis: verum

end;

suppose A33: ( not n is zero & a <> 0 & (omega -exponent (CantorNF a)) . 0 <> b ) ; :: thesis: (n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a

then A34: (omega -exponent (CantorNF a)) . 0 in b by A2, XBOOLE_0:def 8, ORDINAL1:11;
0 c< n by A33, XBOOLE_1:2, XBOOLE_0:def 8;
then A35: ( 0 in n & n in omega ) by ORDINAL1:11, ORDINAL1:def 12;
A36: omega -exponent (CantorNF (n *^ (exp (omega,b)))) = omega -exponent <%(n *^ (exp (omega,b)))%> by A33, Th69
.= <%(omega -exponent (n *^ (exp (omega,b))))%> by Th46
.= <%b%> by A35, ORDINAL5:58 ;
then A37: rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) = {b} by AFINSQ_1:33;
(rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) /\ (rng (omega -exponent (CantorNF a))) = {}

proof

assume (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) /\ (rng (omega -exponent (CantorNF a))) <> {} ; :: thesis: contradiction
then consider y being object such that
A38: y in (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) /\ (rng (omega -exponent (CantorNF a))) by XBOOLE_0:def 1;
A39: ( y in rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) & y in rng (omega -exponent (CantorNF a)) ) by A38, XBOOLE_0:def 4;
then y = b by A37, TARSKI:def 1;
then consider x being object such that
A40: ( x in dom (omega -exponent (CantorNF a)) & (omega -exponent (CantorNF a)) . x = b ) by A39, FUNCT_1:def 3;
reconsider x = x as Ordinal by A40;
x <> 0 by A34, A40;
then 0 c< x by XBOOLE_1:2, XBOOLE_0:def 8;
then A41: 0 in x by ORDINAL1:11;
A42: x in dom (CantorNF a) by A40, Def1;
then omega -exponent ((CantorNF a) . x) in omega -exponent ((CantorNF a) . 0) by A41, ORDINAL5:def 11;
then b in omega -exponent ((CantorNF a) . 0) by A40, A42, Def1;
hence contradiction by A34, A41, A42, Def1, ORDINAL1:10; :: thesis: verum

end;

then A43: rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) misses rng (omega -exponent (CantorNF a)) by XBOOLE_0:def 7;
A44: dom C = card (dom (omega -exponent C)) by Def1
.= card (rng (omega -exponent C)) by CARD_1:70
.= (card (rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))))) +` (card (rng (omega -exponent (CantorNF a)))) by A4, A43, CARD_2:35
.= (card (dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))))) +` (card (rng (omega -exponent (CantorNF a)))) by CARD_1:70
.= (dom (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) +` (card (dom (omega -exponent (CantorNF a)))) by CARD_1:70
.= (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + (dom (CantorNF a)) by Def1
.= 1 + (dom (CantorNF a)) by A36, AFINSQ_1:34
.= (len <%(n *^ (exp (omega,b)))%>) + (len (CantorNF a)) by AFINSQ_1:34
.= dom (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) by AFINSQ_1:17 ;
for x being object st x in dom C holds
C . x = (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x

proof

let x be object ; :: thesis: ( x in dom C implies C . x = (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x )
assume A45: x in dom C ; :: thesis: C . x = (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x
for c, d being Ordinal st c in d & d in dom ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) holds
((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c

proof

let c, d be Ordinal; :: thesis: ( c in d & d in dom ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) implies ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c )
assume A46: ( c in d & d in dom ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) ) ; :: thesis: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c
then A47: c in dom ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) by ORDINAL1:10;
then reconsider m1 = c, m2 = d as Nat by A46;

per cases ( m1 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) or ex k1 being Nat st
( k1 in dom (omega -exponent (CantorNF a)) & m1 = (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k1 ) ) by A47, AFINSQ_1:20;

suppose A48: m1 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) ; :: thesis: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c

then m1 in 1 by A36, AFINSQ_1:34;
then A49: m1 = 0 by CARD_1:49, TARSKI:def 1;
A50: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . m1 = (omega -exponent (CantorNF (n *^ (exp (omega,b))))) . m1 by A48, AFINSQ_1:def 3
.= b by A36, A49 ;
not m2 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b)))))

proof

assume m2 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) ; :: thesis: contradiction
then m2 in 1 by A36, AFINSQ_1:34;
hence contradiction by A46, CARD_1:49, TARSKI:def 1; :: thesis: verum

end;

then consider k2 being Nat such that
A51: ( k2 in dom (omega -exponent (CantorNF a)) & m2 = (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k2 ) by A46, AFINSQ_1:20;
A52: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . m2 = (omega -exponent (CantorNF a)) . k2 by A51, AFINSQ_1:def 3;

per cases ( k2 = 0 or k2 <> 0 ) ;

suppose k2 = 0 ; :: thesis: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c

hence ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c by A34, A50, A52; :: thesis: verum

end;

suppose k2 <> 0 ; :: thesis: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c

then 0 c< k2 by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in k2 by ORDINAL1:11;
then (omega -exponent (CantorNF a)) . k2 in (omega -exponent (CantorNF a)) . 0 by A51, ORDINAL5:def 1;
hence ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c by A34, A50, A52, ORDINAL1:10; :: thesis: verum

end;

end;

end;

suppose ex k1 being Nat st
( k1 in dom (omega -exponent (CantorNF a)) & m1 = (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k1 ) ; :: thesis: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c

then consider k1 being Nat such that
A53: ( k1 in dom (omega -exponent (CantorNF a)) & m1 = (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k1 ) ;
A54: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . m1 = (omega -exponent (CantorNF a)) . k1 by A53, AFINSQ_1:def 3;
not m2 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b)))))

proof

assume m2 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) ; :: thesis: contradiction
then A55: m2 in 1 by A36, AFINSQ_1:34;

per cases ( k1 = 0 or k1 <> 0 ) ;

suppose k1 = 0 ; :: thesis: contradiction

hence contradiction by A46, A36, A53, A55, AFINSQ_1:34; :: thesis: verum

end;

suppose k1 <> 0 ; :: thesis: contradiction

then len (omega -exponent (CantorNF (n *^ (exp (omega,b))))) < (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k1 by NAT_1:16;
then 1 < m1 by A36, A53, AFINSQ_1:34;
then 1 in Segm m1 by NAT_1:44;
hence contradiction by A46, A55, ORDINAL1:10; :: thesis: verum

end;

end;

end;

then consider k2 being Nat such that
A56: ( k2 in dom (omega -exponent (CantorNF a)) & m2 = (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k2 ) by A46, AFINSQ_1:20;
A57: ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . m2 = (omega -exponent (CantorNF a)) . k2 by A56, AFINSQ_1:def 3;
m1 in Segm m2 by A46;
then ((len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k1) - (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) < ((len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k2) - (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) by A53, A56, NAT_1:44, XREAL_1:14;
then k1 in Segm k2 by NAT_1:44;
hence ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . d in ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) . c by A54, A56, A57, ORDINAL5:def 1; :: thesis: verum

end;

end;

end;

then A58: (omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a)) is decreasing by ORDINAL5:def 1;
rng ((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a))) = rng (omega -exponent C) by A4, AFINSQ_1:26;
then A59: omega -exponent C = (omega -exponent (CantorNF (n *^ (exp (omega,b))))) ^ (omega -exponent (CantorNF a)) by A58, Th34;

per cases ( x = 0 or x <> 0 ) ;

suppose A60: x = 0 ; :: thesis: C . x = (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x

A61: omega -exponent (C . x) = (omega -exponent C) . x by A45, Def1
.= b by A36, A59, A60, AFINSQ_1:35 ;
then omega -exponent (C . x) in rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by A37, TARSKI:def 1;
then A62: omega -exponent (C . x) in (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) \ (rng (omega -exponent (CantorNF a))) by A43, XBOOLE_1:83;
A63: (omega -exponent (CantorNF (n *^ (exp (omega,b))))) . 0 = b by A36;
dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) = 1 by A36, AFINSQ_1:34;
then A64: 0 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by CARD_1:49, TARSKI:def 1;
omega -leading_coeff (C . x) = (omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . (((omega -exponent (CantorNF (n *^ (exp (omega,b))))) ") . (omega -exponent (C . x))) by A5, A45, A62
.= (omega -leading_coeff (CantorNF (n *^ (exp (omega,b))))) . 0 by A61, A63, A64, FUNCT_1:34
.= (omega -leading_coeff <%(n *^ (exp (omega,b)))%>) . 0 by A33, Th69
.= <%(omega -leading_coeff (n *^ (exp (omega,b))))%> . 0 by Th60
.= n by Th57, ORDINAL1:def 12 ;
hence C . x = n *^ (exp (omega,b)) by A45, A61, Th64
.= (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x by A60, AFINSQ_1:35 ;
:: thesis: verum

end;

suppose A66: x <> 0 ; :: thesis: C . x = (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x

then not x in 1 by CARD_1:49, TARSKI:def 1;
then A67: not x in len (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by A36, AFINSQ_1:34;
A68: x in dom (omega -exponent C) by A45, Def1;
then consider k being Nat such that
A69: ( k in dom (omega -exponent (CantorNF a)) & x = (len (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) + k ) by A59, A67, AFINSQ_1:20;
omega -exponent (C . x) <> b

proof

0 in 1 by CARD_1:49, TARSKI:def 1;
then A70: 0 in dom (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by A36, AFINSQ_1:34;
assume omega -exponent (C . x) = b ; :: thesis: contradiction
then A71: (omega -exponent C) . x = (omega -exponent (CantorNF (n *^ (exp (omega,b))))) . 0 by A36, A45, Def1
.= (omega -exponent C) . 0 by A59, A70, AFINSQ_1:def 3 ;
0 in dom (omega -exponent C) by A59, A70, TARSKI:def 3, AFINSQ_1:21;
hence contradiction by A66, A68, A71, FUNCT_1:def 4; :: thesis: verum

end;

then A72: not omega -exponent (C . x) in rng (omega -exponent (CantorNF (n *^ (exp (omega,b))))) by A37, TARSKI:def 1;
A73: k in dom (CantorNF a) by A69, Def1;
A74: x = 1 + k by A36, A69, AFINSQ_1:34
.= (len <%(n *^ (exp (omega,b)))%>) + k by AFINSQ_1:34 ;
x in dom (omega -exponent C) by A45, Def1;
then (omega -exponent C) . x in rng (omega -exponent C) by FUNCT_1:3;
then omega -exponent (C . x) in (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) \/ (rng (omega -exponent (CantorNF a))) by A4, A45, Def1;
then omega -exponent (C . x) in rng (omega -exponent (CantorNF a)) by A72, XBOOLE_0:def 3;
then omega -exponent (C . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF (n *^ (exp (omega,b)))))) by A72, XBOOLE_0:def 5;
then omega -leading_coeff (C . x) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . x))) by A5, A45
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent C) . x)) by A45, Def1
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . k)) by A59, A69, AFINSQ_1:def 3
.= (omega -leading_coeff (CantorNF a)) . k by A69, FUNCT_1:34 ;
hence C . x = ((omega -leading_coeff (CantorNF a)) . k) *^ (exp (omega,(omega -exponent (C . x)))) by A45, Th64
.= ((omega -leading_coeff (CantorNF a)) . k) *^ (exp (omega,((omega -exponent C) . x))) by A45, Def1
.= ((omega -leading_coeff (CantorNF a)) . k) *^ (exp (omega,((omega -exponent (CantorNF a)) . k))) by A59, A69, AFINSQ_1:def 3
.= (CantorNF a) . k by A73, Th65
.= (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) . x by A73, A74, AFINSQ_1:def 3 ;
:: thesis: verum

end;

end;

end;

hence (n *^ (exp (omega,b))) (+) a = Sum^ (<%(n *^ (exp (omega,b)))%> ^ (CantorNF a)) by A3, A44, FUNCT_1:2
.= (n *^ (exp (omega,b))) +^ (Sum^ (CantorNF a)) by ORDINAL5:55
.= (n *^ (exp (omega,b))) +^ a ;
:: thesis: verum

end;

end;