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 Nat st

for r being 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 Nat st

for r being 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 Nat st

for r being 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;

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 object 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 object such that

A8: i in dom s and

A9: s . i = a by A5, FUNCT_1:def 3;

reconsider i = i as Nat by A8;

assume for p being Nat ex r being Nat st

( p <= r & not s . p = s . r ) ; :: thesis: contradiction

then consider r being 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, Th8;

then A12: s . r in the InternalRel of R -Seg a by A9, A11, WELLORD1:1;

reconsider r = r as Element of NAT by ORDINAL1:def 12;

s . r in rng s by A4, FUNCT_1:3;

hence contradiction by A7, A12, XBOOLE_0:def 4; :: thesis: verum

ex p being Nat st

for r being 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 Nat st

for r being 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 Nat st

for r being 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;

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 object 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 object such that

A8: i in dom s and

A9: s . i = a by A5, FUNCT_1:def 3;

reconsider i = i as Nat by A8;

assume for p being Nat ex r being Nat st

( p <= r & not s . p = s . r ) ; :: thesis: contradiction

then consider r being 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, Th8;

then A12: s . r in the InternalRel of R -Seg a by A9, A11, WELLORD1:1;

reconsider r = r as Element of NAT by ORDINAL1:def 12;

s . r in rng s by A4, FUNCT_1:3;

hence contradiction by A7, A12, XBOOLE_0:def 4; :: thesis: verum