let f be Sequence; :: thesis: ( f is decreasing implies f is finite )
assume A1: for a, b being Ordinal st a in b & b in dom f holds
f . b in f . a ; :: according to ORDINAL5:def 1 :: thesis: f is finite
set X = f .: omega;
assume f is infinite ; :: thesis: contradiction
then A2: ( 0 in omega & omega c= dom f ) by Th5;
then f . 0 in f .: omega by FUNCT_1:def 6;
then consider x being set such that
A3: ( x in f .: omega & f .: omega misses x ) by XREGULAR:1;
consider a being object such that
A4: ( a in dom f & a in omega & x = f . a ) by A3, FUNCT_1:def 6;
reconsider a = a as Ordinal by A4;
A5: succ a in omega by A4, ORDINAL1:28;
then ( a in succ a & succ a in dom f ) by A2, ORDINAL1:6;
then ( f . (succ a) in x & f . (succ a) in f .: omega ) by A1, A4, A5, FUNCT_1:def 6;
hence contradiction by A3, XBOOLE_0:3; :: thesis: verum