let a be non empty Ordinal; :: thesis: for n being non zero Nat st omega -exponent (last (CantorNF a)) <> 0 holds
CantorNF (a +^ n) = (CantorNF a) ^ <%n%>
let n be non zero Nat; :: thesis: ( omega -exponent (last (CantorNF a)) <> 0 implies CantorNF (a +^ n) = (CantorNF a) ^ <%n%> )
assume omega -exponent (last (CantorNF a)) <> 0 ; :: thesis: CantorNF (a +^ n) = (CantorNF a) ^ <%n%>
then 0 c< omega -exponent (last (CantorNF a)) by XBOOLE_1:2, XBOOLE_0:def 8;
then A1: 0 in omega -exponent (last (CantorNF a)) by ORDINAL1:11;
thus CantorNF (a +^ n) = CantorNF (a +^ (n *^ 1)) by ORDINAL2:39
.= CantorNF (a +^ (n *^ (exp (omega,0)))) by ORDINAL2:43
.= (CantorNF a) ^ <%(n *^ (exp (omega,0)))%> by A1, Th73
.= (CantorNF a) ^ <%(n *^ 1)%> by ORDINAL2:43
.= (CantorNF a) ^ <%n%> by ORDINAL2:39 ; :: thesis: verum