let f be T-Sequence; :: thesis: ( f is decreasing implies f is finite )
assume A1: for a, b being ordinal number 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 not f is finite ; :: thesis: contradiction
then A2: ( 0 in omega & omega c= dom f ) by ThO;
then f . 0 in f .: omega by FUNCT_1:def 12;
then consider x being set such that
A3: ( x in f .: omega & ( for y being set holds
( not y in f .: omega or not y in x ) ) ) by TARSKI:7;
consider a being set such that
A4: ( a in dom f & a in omega & x = f . a ) by A3, FUNCT_1:def 12;
reconsider a = a as Ordinal by A4;
A5: succ a in omega by A4, ORDINAL1:41;
then ( a in succ a & succ a in dom f ) by A2, ORDINAL1:10;
then ( f . (succ a) in x & f . (succ a) in f .: omega ) by A1, A4, A5, FUNCT_1:def 12;
hence contradiction by A3; :: thesis: verum