let f be Ordinal-Sequence; :: thesis: ( f is Cantor-normal-form implies f is decreasing )
assume that
for a being ordinal number st a in dom f holds
f . a is Cantor-component and
A1: for a, b being ordinal number 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 number ; :: according to ORDINAL5:def 1 :: thesis: for b being ordinal number st a in b & b in dom f holds
f . b in f . a
let b be ordinal number ; :: 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 Th43d; :: thesis: verum