let f be non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); :: thesis: for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Nat st i < len f & 1 < i holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> f /. 1
let g be non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st i < len f & 1 < i holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> f /. 1
let i, j be Nat; :: thesis: ( i < len f & 1 < i implies for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> f /. 1 )
assume that
A1: i < len f and
A2: 1 < i ; :: thesis: for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> f /. 1
A3: 1 < i + 1 by A2, XREAL_1:29;
A4: (LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))} by A1, A2, Th32;
i + 1 <= len f by A1, NAT_1:13;
then A5: i + 1 in dom f by A3, FINSEQ_3:25;
A6: LSeg ((f ^' g),i) = LSeg (f,i) by A1, Th28;
let x be Point of (TOP-REAL 2); :: thesis: ( x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) implies x <> f /. 1 )
assume x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) ; :: thesis: x <> f /. 1
then A7: x in LSeg (f,i) by A6, XBOOLE_0:def 4;
A8: 1 in dom f by FINSEQ_5:6;
assume A9: x = f /. 1 ; :: thesis: contradiction
x = f . 1 by A9, A8, PARTFUN1:def 6;
then x in rng f by A8, FUNCT_1:3;
then x in (LSeg (f,i)) /\ (rng f) by A7, XBOOLE_0:def 4;
then A10: ( x = f /. i or x = f /. (i + 1) ) by A4, TARSKI:def 2;
i in dom f by A1, A2, FINSEQ_3:25;
hence contradiction by A2, A9, A8, A10, A3, A5, PARTFUN2:10; :: thesis: verum