let i be 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:134;
A6: i + 1 in dom f by A2, A3, SEQ_4:134;
A7: f is one-to-one by A1;
A8: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, A3, TOPREAL1:def 3;
f /. i <> f /. (i + 1)

proof

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

end;

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