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 that
A1: f is being_S-Seq and
A2: 1 <= i and
A3: i + 1 <= len f and
A4: P = LSeg f,i ; :: thesis: P is_an_arc_of f /. i,f /. (i + 1)
A5: i in dom f by A2, A3, SEQ_4:151;
A6: i + 1 in dom f by A2, A3, SEQ_4:151;
A7: f is one-to-one by A1, TOPREAL1:def 10;
A8: LSeg f,i = LSeg (f /. i),(f /. (i + 1)) by A2, A3, TOPREAL1:def 5;
f /. i <> f /. (i + 1)

proof

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

end;

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