let b be ordinal number ; :: thesis: for n being natural number st 0 in n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form
let n be natural number ; :: thesis: ( 0 in n implies <%(n *^ (exp (omega,b)))%> is Cantor-normal-form )
assume A1: 0 in n ; :: thesis: <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
set A = <%(n *^ (exp (omega,b)))%>;
A2: ( dom <%(n *^ (exp (omega,b)))%> = 1 & <%(n *^ (exp (omega,b)))%> . 0 = n *^ (exp (omega,b)) ) by AFINSQ_1:def 4;

hereby :: according to ORDINAL5:def 11 :: thesis: for a, b being ordinal number st a in b & b in dom <%(n *^ (exp (omega,b)))%> holds
omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a)

let a be ordinal number ; :: thesis: ( a in dom <%(n *^ (exp (omega,b)))%> implies <%(n *^ (exp (omega,b)))%> . a is Cantor-component )
assume a in dom <%(n *^ (exp (omega,b)))%> ; :: thesis: <%(n *^ (exp (omega,b)))%> . a is Cantor-component
then ( a = 0 & 0 in 1 ) by A2, ORDINAL3:15, TARSKI:def 1;
hence <%(n *^ (exp (omega,b)))%> . a is Cantor-component by A1, A2, Def9; :: thesis: verum

end;

let a, b be ordinal number ; :: thesis: ( a in b & b in dom <%(n *^ (exp (omega,b)))%> implies omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a) )
assume A3: a in b ; :: thesis: ( not b in dom <%(n *^ (exp (omega,b)))%> or omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a) )
assume b in dom <%(n *^ (exp (omega,b)))%> ; :: thesis: omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a)
hence omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a) by A3, A2, ORDINAL3:15, TARSKI:def 1; :: thesis: verum