let i be Element of NAT ; :: thesis: for f being FinSequence of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg f,i holds
P is_an_arc_of f /. i,f /. (i + 1)
let f be FinSequence of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2) st f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg f,i holds
P is_an_arc_of f /. i,f /. (i + 1)
let P be Subset of (TOP-REAL 2); :: thesis: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg f,i implies P is_an_arc_of f /. i,f /. (i + 1) )
assume A1: ( f is being_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg f,i ) ; :: thesis: P is_an_arc_of f /. i,f /. (i + 1)
then A2: ( i in dom f & i + 1 in dom f ) by GOBOARD2:3;
A3: f is one-to-one by A1, TOPREAL1:def 10;
A4: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A1, TOPREAL1:def 5;
f /. i <> f /. (i + 1)

proof

assume f /. i = f /. (i + 1) ; :: thesis: contradiction
then i = i + 1 by A2, A3, PARTFUN2:17;
hence contradiction ; :: thesis: verum

end;

hence P is_an_arc_of f /. i,f /. (i + 1) by A1, A4, TOPREAL1:15; :: thesis: verum