let a, b be Ordinal; :: thesis: 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))
let n be non zero Nat; :: thesis: ( n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) implies (CantorNF a) . 0 = n *^ (exp (omega,b)) )
assume A1: ( n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) ) ; :: thesis: (CantorNF a) . 0 = n *^ (exp (omega,b))
then A2: a <> {} ;
then consider a0 being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A3: CantorNF a = <%a0%> ^ A0 by ORDINAL5:67;
A4: 0 in n by XBOOLE_1:61, ORDINAL1:11;
n in succ n by ORDINAL1:6;
then 0 in succ n by A4, ORDINAL1:10;
then A5: 0 in n + 1 by Lm5;
( n in omega & n + 1 in omega ) by ORDINAL1:def 12;
then A7: omega -exponent (n *^ (exp (omega,b))) = b by A4, ORDINAL5:58;
omega -exponent ((n + 1) *^ (exp (omega,b))) = b by A5, ORDINAL5:58;
then ( b c= omega -exponent a & omega -exponent a c= b ) by A7, A1, Th22, ORDINAL1:def 2;
then A9: b = omega -exponent (Sum^ (CantorNF a)) by XBOOLE_0:def 10
.= omega -exponent ((CantorNF a) . 0) by Th44 ;
0 in dom (CantorNF a) by A2, XBOOLE_1:61, ORDINAL1:11;
then A10: (CantorNF a) . 0 is Cantor-component by ORDINAL5:def 11;
then reconsider m = omega -leading_coeff ((CantorNF a) . 0) as Nat ;
A11: (CantorNF a) . 0 = m *^ (exp (omega,b)) by A9, A10, Th59;
A12: (CantorNF a) . 0 = a0 by A3, AFINSQ_1:35;
m = n
proof
assume m <> n ; :: thesis: contradiction
per cases then ( m < n or n < m ) by XXREAL_0:1;
suppose m < n ; :: thesis: contradiction
then m + 1 <= n by NAT_1:13;
then Segm (m + 1) c= Segm n by NAT_1:39;
then (m + 1) *^ (exp (omega,b)) c= n *^ (exp (omega,b)) by ORDINAL2:41;
then (m +^ 1) *^ (exp (omega,b)) c= n *^ (exp (omega,b)) by CARD_2:36;
then A13: (m *^ (exp (omega,b))) +^ (1 *^ (exp (omega,b))) c= n *^ (exp (omega,b)) by ORDINAL3:46;
Sum^ A0 in exp (omega,b) by A3, A9, A12, Th43;
then Sum^ A0 in 1 *^ (exp (omega,b)) by ORDINAL2:39;
then (m *^ (exp (omega,b))) +^ (Sum^ A0) in (m *^ (exp (omega,b))) +^ (1 *^ (exp (omega,b))) by ORDINAL2:32;
then a0 +^ (Sum^ A0) in n *^ (exp (omega,b)) by A11, A12, A13;
then Sum^ (CantorNF a) in n *^ (exp (omega,b)) by A3, ORDINAL5:55;
hence contradiction by A1, ORDINAL1:12; :: thesis: verum
end;
end;
end;
hence (CantorNF a) . 0 = n *^ (exp (omega,b)) by A11; :: thesis: verum