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