let f be FinSequence of (); :: thesis: for i being Nat st 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) holds
Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) )
assume that
A1: ( 1 <= i & i + 1 <= len f ) and
A2: f is being_S-Seq and
A3: Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; :: thesis: Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1)
reconsider Q = LSeg (f,i) as non empty Subset of () by A3;
Q = LSeg ((f /. i),(f /. (i + 1))) by ;
then Q c= L~ f by ;
then L~ f meets Q by ;
then A4: Last_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = Last_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th20;
( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by ;
hence Last_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. (i + 1) by ; :: thesis: verum