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 A0: 0 in n ; :: thesis: <%(n *^ (exp omega ,b))%> is Cantor-normal-form
set A = <%(n *^ (exp omega ,b))%>;
A1: ( dom <%(n *^ (exp omega ,b))%> = 1 & <%(n *^ (exp omega ,b))%> . 0 = n *^ (exp omega ,b) ) by AFINSQ_1:def 5;

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 A1, TARSKI:def 1, ORDINAL3:18;
hence <%(n *^ (exp omega ,b))%> . a is Cantor-component by A0, A1, CC; :: 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 A2: 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 A2, A1, TARSKI:def 1, ORDINAL3:18; :: thesis: verum