let n be Nat; :: thesis: for h being FinSequence of (TOP-REAL n) st len h >= 2 holds
h /. (len h) in LSeg (h,((len h) -' 1))
let h be FinSequence of (TOP-REAL n); :: thesis: ( len h >= 2 implies h /. (len h) in LSeg (h,((len h) -' 1)) )
set i = len h;
assume A1: len h >= 2 ; :: thesis: h /. (len h) in LSeg (h,((len h) -' 1))
then A2: 2 - 1 <= (len h) - 1 by XREAL_1:9;
((len h) -' 1) + 1 = len h by A1, XREAL_1:235, XXREAL_0:2;
hence h /. (len h) in LSeg (h,((len h) -' 1)) by A2, TOPREAL1:21; :: thesis: verum