let n be Element of 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: ((len h) -' 1) + 1 = len h by XREAL_1:237, XXREAL_0:2;
2 - 1 <= (len h) - 1 by A1, XREAL_1:11;
hence h /. (len h) in LSeg h,((len h) -' 1) by A2, TOPREAL1:27; :: thesis: verum