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

( 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