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

First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i )

assume that

A1: ( 1 <= i & i + 1 <= len f ) and

A2: f is being_S-Seq and

A3: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; :: thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i

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 3;

then Q c= L~ f by A1, SPPOL_2:16;

then L~ f meets Q by A3, XBOOLE_0:3;

then A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th19;

( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15;

hence First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i by A4, Th7; :: thesis: verum

First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len f & f is being_S-Seq & First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) implies First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i )

assume that

A1: ( 1 <= i & i + 1 <= len f ) and

A2: f is being_S-Seq and

A3: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) in LSeg (f,i) ; :: thesis: First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i

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 3;

then Q c= L~ f by A1, SPPOL_2:16;

then L~ f meets Q by A3, XBOOLE_0:3;

then A4: First_Point ((L~ f),(f /. 1),(f /. (len f)),Q) = First_Point (Q,(f /. i),(f /. (i + 1)),Q) by A1, A2, A3, Th19;

( Q is closed & Q is_an_arc_of f /. i,f /. (i + 1) ) by A1, A2, JORDAN5B:15;

hence First_Point ((L~ f),(f /. 1),(f /. (len f)),(LSeg (f,i))) = f /. i by A4, Th7; :: thesis: verum