let f be FinSequence of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2)
for i being Nat st i + 1 <= len (f -: p) holds
LSeg ((f -: p),i) = LSeg (f,i)
let p be Point of (TOP-REAL 2); :: thesis: for i being Nat st i + 1 <= len (f -: p) holds
LSeg ((f -: p),i) = LSeg (f,i)
let i be Nat; :: thesis: ( i + 1 <= len (f -: p) implies LSeg ((f -: p),i) = LSeg (f,i) )
f -: p = f | (p .. f) by FINSEQ_5:def 1;
hence ( i + 1 <= len (f -: p) implies LSeg ((f -: p),i) = LSeg (f,i) ) by Th3; :: thesis: verum