let f be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of 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 Element of 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 (TOP-REAL 2) by A3;
Q = LSeg (f /. i),(f /. (i + 1)) by A1, TOPREAL1:def 5;
then Q c= L~ f by A1, SPPOL_2:16;
then L~ f meets Q by A3, XBOOLE_0:3;
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, SPPOL_1:40;
( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15, SPPOL_1:40;
hence Last_Point (L~ f),(f /. 1),(f /. (len f)),(LSeg f,i) = f /. (i + 1) by A4, Th7; :: thesis: verum