let f be FinSequence of (TOP-REAL 2); :: 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 A3, NAT_1:10;

A6: len f >= 2 by A1, TOPREAL1:def 8;

then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;

defpred S_{1}[ 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 S_{1}[l] holds

S_{1}[l + 1]
_{1}[ 0 ]
_{1}[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

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 A3, NAT_1:10;

A6: len f >= 2 by A1, TOPREAL1:def 8;

then reconsider P = L~ f as non empty Subset of (TOP-REAL 2) by TOPREAL1:23;

defpred S

A7: for l being Nat st S

S

proof

A13:
S
let l be Nat; :: thesis: ( S_{1}[l] implies S_{1}[l + 1] )

assume A8: S_{1}[l]
; :: thesis: S_{1}[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 A10, XXREAL_0:2;

then LE f /. (i + l),f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A1, A12, Th23;

hence LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A8, A10, A11, A9, Th13, XXREAL_0:2; :: thesis: verum

end;assume A8: S

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 A10, XXREAL_0:2;

then LE f /. (i + l),f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A1, A12, Th23;

hence LE f /. i,f /. (i + (l + 1)),P,f /. 1,f /. (len f) by A8, A10, A11, A9, Th13, XXREAL_0:2; :: thesis: verum

proof

A14:
for l being Nat holds S
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 A6, Th9, GOBOARD1:1; :: thesis: verum

end;then i in dom f by FINSEQ_3:25;

hence LE f /. i,f /. (i + 0),P,f /. 1,f /. (len f) by A6, Th9, GOBOARD1:1; :: thesis: verum

thus LE f /. i,f /. j, L~ f,f /. 1,f /. (len f) by A2, A4, A5, A14; :: thesis: verum