let b be Ordinal; :: thesis: for n being Nat st 0 in Segm n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form
let n be Nat; :: thesis: ( 0 in Segm n implies <%(n *^ (exp (omega,b)))%> is Cantor-normal-form )
assume A1: 0 in Segm n ; :: thesis: <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
set A = <%(n *^ (exp (omega,b)))%>;
A2: ( dom <%(n *^ (exp (omega,b)))%> = Segm 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 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; :: 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 Segm 1 ) by A2, ORDINAL3:15, TARSKI:def 1;
hence <%(n *^ (exp (omega,b)))%> . a is Cantor-component by A1; :: thesis: verum
end;
let a, b be Ordinal; :: 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