let A be non empty Cantor-normal-form Ordinal-Sequence; :: thesis: for b being Ordinal
for n being non zero Nat st omega -exponent (last A) <> 0 holds
A ^ <%n%> is Cantor-normal-form
let b be Ordinal; :: thesis: for n being non zero Nat st omega -exponent (last A) <> 0 holds
A ^ <%n%> is Cantor-normal-form
let n be non zero Nat; :: thesis: ( omega -exponent (last A) <> 0 implies A ^ <%n%> is Cantor-normal-form )
assume omega -exponent (last A) <> 0 ; :: thesis: A ^ <%n%> is Cantor-normal-form
then 0 c< omega -exponent (last A) by XBOOLE_1:2, XBOOLE_0:def 8;
then A1: 0 in omega -exponent (last A) by ORDINAL1:11;
A ^ <%(n *^ (exp (omega,0)))%> = A ^ <%(n *^ 1)%> by ORDINAL2:43
.= A ^ <%n%> by ORDINAL2:39 ;
hence A ^ <%n%> is Cantor-normal-form by A1, Th37; :: thesis: verum