let A be non empty Cantor-normal-form Ordinal-Sequence; :: thesis: for b being Ordinal
for n being non zero Nat st omega -exponent (A . 0) in b holds
<%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form
let b be Ordinal; :: thesis: for n being non zero Nat st omega -exponent (A . 0) in b holds
<%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form
let n be non zero Nat; :: thesis: ( omega -exponent (A . 0) in b implies <%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form )
assume A1: omega -exponent (A . 0) in b ; :: thesis: <%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form
0 c< n by XBOOLE_1:2, XBOOLE_0:def 8;
then ( 0 in n & n in omega ) by ORDINAL1:11, ORDINAL1:def 12;
then omega -exponent (A . 0) in omega -exponent (n *^ (exp (omega,b))) by A1, ORDINAL5:58;
then omega -exponent (A . 0) in omega -exponent (last ({} ^ <%(n *^ (exp (omega,b)))%>)) by AFINSQ_1:92;
hence <%(n *^ (exp (omega,b)))%> ^ A is Cantor-normal-form by Th33; :: thesis: verum