let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL n) st 2 <= len f holds
( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f )
let f be FinSequence of (TOP-REAL n); :: thesis: ( 2 <= len f implies ( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f ) )
assume A1: 2 <= len f ; :: thesis: ( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f )
then A2: 1 + 1 <= len f ;
then A3: LSeg (f,1) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
f /. 1 in LSeg ((f /. 1),(f /. (1 + 1))) by RLTOPSP1:68;
then f /. 1 in LSeg (f,1) by A1, TOPREAL1:def 3;
then f /. 1 in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A3, TARSKI:def 4;
then A4: f /. 1 in L~ f by TOPREAL1:def 4;
A5: ((len f) -' 1) + 1 = len f by A2, NAT_D:46, XREAL_1:235;
A6: 1 <= (len f) -' 1 by A2, NAT_D:49;
then A7: LSeg (f,((len f) -' 1)) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A5;
f /. (len f) in LSeg ((f /. ((len f) -' 1)),(f /. (((len f) -' 1) + 1))) by A5, RLTOPSP1:68;
then f /. (len f) in LSeg (f,((len f) -' 1)) by A6, A5, TOPREAL1:def 3;
then f /. (len f) in union { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } by A7, TARSKI:def 4;
then A8: f /. (len f) in L~ f by TOPREAL1:def 4;
1 <= len f by A2, NAT_D:46;
hence ( f . 1 in L~ f & f /. 1 in L~ f & f . (len f) in L~ f & f /. (len f) in L~ f ) by A4, A8, FINSEQ_4:15; :: thesis: verum