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