let a be non empty Ordinal; :: thesis: for n, m being non zero Nat holds <%(n *^ (exp (omega,a))),m%> is Cantor-normal-form
let n, m be non zero Nat; :: thesis: <%(n *^ (exp (omega,a))),m%> 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 A1: omega -exponent (n *^ (exp (omega,a))) = a by ORDINAL5:58;
A2: omega -exponent m = 0 by Th21, ORDINAL1:def 12;
0 c< a by XBOOLE_1:2, XBOOLE_0:def 8;
hence <%(n *^ (exp (omega,a))),m%> is Cantor-normal-form by A1, A2, Th35, ORDINAL1:11; :: thesis: verum