let R be non empty transitive RelStr ; :: thesis: for f being sequence of R st f is non-increasing holds
for j, i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R
let f be sequence of R; :: thesis: ( f is non-increasing implies for j, i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R )
assume A1: f is non-increasing ; :: thesis: for j, i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R
set IR = the InternalRel of R;
set CR = the carrier of R;
A2: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 3;
defpred S₁[ Nat] means for i being Nat st i < $1 holds
[(f . $1),(f . i)] in the InternalRel of R;
A3: S₁[ 0 ] ;

now

let j be Nat; :: thesis: ( ( for i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R ) implies for i being Nat st i < j + 1 holds
[(f . (j + 1)),(f . i)] in the InternalRel of R )
assume A4: for i being Nat st i < j holds
[(f . j),(f . i)] in the InternalRel of R ; :: thesis: for i being Nat st i < j + 1 holds
[(f . (j + 1)),(f . i)] in the InternalRel of R
let i be Nat; :: thesis: ( i < j + 1 implies [(f . (j + 1)),(f . i)] in the InternalRel of R )
assume A5: i < j + 1 ; :: thesis: [(f . (j + 1)),(f . i)] in the InternalRel of R

now

per cases ( i > j or i = j or i < j ) by XXREAL_0:1;

suppose i > j ; :: thesis: [(f . (j + 1)),(f . i)] in the InternalRel of R

hence [(f . (j + 1)),(f . i)] in the InternalRel of R by A5, NAT_1:13; :: thesis: verum

end;

suppose i = j ; :: thesis: [(f . (j + 1)),(f . i)] in the InternalRel of R

hence [(f . (j + 1)),(f . i)] in the InternalRel of R by A1, Def3; :: thesis: verum

end;

suppose i < j ; :: thesis: [(f . (j + 1)),(f . i)] in the InternalRel of R

then A6: [(f . j),(f . i)] in the InternalRel of R by A4;
[(f . (j + 1)),(f . j)] in the InternalRel of R by A1, Def3;
hence [(f . (j + 1)),(f . i)] in the InternalRel of R by A2, A6, RELAT_2:def 8; :: thesis: verum

end;

end;

end;

hence [(f . (j + 1)),(f . i)] in the InternalRel of R ; :: thesis: verum

end;

then A7: for j being Nat st S₁[j] holds
S₁[j + 1] ;
thus for j being Nat holds S₁[j] from NAT_1:sch 2(A3, A7); :: thesis: verum