let f be FinSequence of (TOP-REAL 2); 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; ( 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
; 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 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;
( S1[l] implies S1[l + 1] )
assume A8:
S1[
l]
;
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
;
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;
verum
end;
A13:
S1[ 0 ]
proof
assume
( 1
<= i &
i + 0 <= len f )
;
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;
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; verum