let f be FinSequence of (); :: thesis: for i, j being Nat st f is being_S-Seq & 1 <= i & i <= j & j <= len f holds
LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)

let i, j be Nat; :: thesis: ( f is being_S-Seq & 1 <= i & i <= j & j <= len f implies LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) )
assume that
A1: f is being_S-Seq and
A2: 1 <= i and
A3: i <= j and
A4: j <= len f ; :: thesis: LE f /. i,f /. j, L~ f,f /. 1,f /. (len f)
consider k being Nat such that
A5: i + k = j by ;
A6: len f >= 2 by ;
then reconsider P = L~ f as non empty Subset of () by TOPREAL1:23;
defpred S1[ Nat] means ( 1 <= i & i + \$1 <= len f implies LE f /. i,f /. (i + \$1),P,f /. 1,f /. (len f) );
A7: for l being Nat st S1[l] holds
S1[l + 1]
proof
let l be Nat; :: thesis: ( S1[l] implies S1[l + 1] )
assume A8: S1[l] ; :: thesis: S1[l + 1]
A9: i + l <= (i + l) + 1 by NAT_1:11;
assume that
A10: 1 <= i and
A11: i + (l + 1) <= len f ; :: thesis: LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f)
A12: (i + l) + 1 <= len f by A11;
i <= i + l by NAT_1:11;
then 1 <= i + l by ;
then LE f /. (i + l),f /. (i + (l + 1)),P,f /. 1,f /. (len f) by ;
hence LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f) by ; :: thesis: verum
end;
A13: S1[ 0 ]
proof
assume ( 1 <= i & i + 0 <= len f ) ; :: thesis: LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f)
then i in dom f by FINSEQ_3:25;
hence LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f) by ; :: thesis: verum
end;
A14: for l being Nat holds S1[l] from NAT_1:sch 2(A13, A7);
thus LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) by A2, A4, A5, A14; :: thesis: verum