let f be Ordinal-Sequence; :: thesis: ( f is Cantor-normal-form implies f is decreasing )
assume that
for a being Ordinal st a in dom f holds
f . a is Cantor-component and
A1: for a, b being Ordinal st a in b & b in dom f holds
omega -exponent (f . b) in omega -exponent (f . a) ; :: according to ORDINAL5:def 11 :: thesis: f is decreasing
let a be Ordinal; :: according to ORDINAL5:def 1 :: thesis: for b being Ordinal st a in b & b in dom f holds
f . b in f . a
let b be Ordinal; :: thesis: ( a in b & b in dom f implies f . b in f . a )
assume ( a in b & b in dom f ) ; :: thesis: f . b in f . a
then omega -exponent (f . b) in omega -exponent (f . a) by A1;
hence f . b in f . a by Th63; :: thesis: verum