let R be non empty transitive RelStr ; :: thesis: for s being sequence of R st R is well_founded & s is non-increasing holds
ex p being Element of NAT st
for r being Element of NAT st p <= r holds
s . p = s . r
let s be sequence of R; :: thesis: ( R is well_founded & s is non-increasing implies ex p being Element of NAT st
for r being Element of NAT st p <= r holds
s . p = s . r )
assume that
A1: R is well_founded and
A2: s is non-increasing ; :: thesis: ex p being Element of NAT st
for r being Element of NAT st p <= r holds
s . p = s . r
set cr = the carrier of R;
set ir = the InternalRel of R;
A3: the InternalRel of R is_well_founded_in the carrier of R by A1, WELLFND1:def 2;
A4: dom s = NAT by FUNCT_2:def 1;
rng s c= the carrier of R by RELAT_1:def 19;
then consider a being set such that
A5: a in rng s and
A6: the InternalRel of R -Seg a misses rng s by A3, WELLORD1:def 3;
A7: (the InternalRel of R -Seg a) /\ (rng s) = {} by A6, XBOOLE_0:def 7;
consider i being set such that
A8: i in dom s and
A9: s . i = a by A5, FUNCT_1:def 5;
reconsider i = i as Element of NAT by A8;
assume for p being Element of NAT ex r being Element of NAT st
( p <= r & not s . p = s . r ) ; :: thesis: contradiction
then consider r being Element of NAT such that
A10: i <= r and
A11: s . i <> s . r ;
i < r by A10, A11, XXREAL_0:1;
then [(s . r),(s . i)] in the InternalRel of R by A2, Th10;
then A12: s . r in the InternalRel of R -Seg a by A9, A11, WELLORD1:def 1;
s . r in rng s by A4, FUNCT_1:12;
hence contradiction by A7, A12, XBOOLE_0:def 4; :: thesis: verum