let A be non empty Cantor-normal-form Ordinal-Sequence; :: thesis: for b being Ordinal
for n being non zero Nat st b in omega -exponent (last A) holds
A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
let b be Ordinal; :: thesis: for n being non zero Nat st b in omega -exponent (last A) holds
A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
let n be non zero Nat; :: thesis: ( b in omega -exponent (last A) implies A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form )
assume A1: b in omega -exponent (last A) ; :: thesis: A ^ <%(n *^ (exp (omega,b)))%> 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 (<%(n *^ (exp (omega,b)))%> . 0) in omega -exponent (last A) by A1, ORDINAL5:58;
hence A ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form by Th33; :: thesis: verum