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 j > len f & j + 1 < len (f ^' g) holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> g /. (len g)
let g be non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st j > len f & j + 1 < len (f ^' g) holds
for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> g /. (len g)
let i, j be Nat; :: thesis: ( j > len f & j + 1 < len (f ^' g) implies for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> g /. (len g) )
assume that
A1: j > len f and
A2: j + 1 < len (f ^' g) ; :: thesis: for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds
x <> g /. (len g)
consider k being Nat such that
A3: j = (len f) + k by A1, NAT_1:10;
(len (f ^' g)) + 1 = (len f) + (len g) by FINSEQ_6:139;
then A4: (j + 1) + 1 < (len f) + (len g) by A2, XREAL_1:6;
reconsider k = k as Nat ;
(j + 1) + 1 = (len f) + ((k + 1) + 1) by A3;
then A5: (k + 1) + 1 < len g by A4, XREAL_1:6;
1 <= (k + 1) + 1 by NAT_1:11;
then A6: (k + 1) + 1 in dom g by A5, FINSEQ_3:25;
let x be Point of (TOP-REAL 2); :: thesis: ( x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) implies x <> g /. (len g) )
assume A7: x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) ; :: thesis: x <> g /. (len g)
A8: len g in dom g by FINSEQ_5:6;
A9: k + 1 <= (k + 1) + 1 by NAT_1:11;
then A10: k + 1 < len g by A5, XXREAL_0:2;
then A11: (LSeg (g,(k + 1))) /\ (rng g) = {(g /. (k + 1)),(g /. ((k + 1) + 1))} by Th32, NAT_1:11;
assume A12: x = g /. (len g) ; :: thesis: contradiction
x = g . (len g) by A12, A8, PARTFUN1:def 6;
then A13: x in rng g by A8, FUNCT_1:3;
1 <= k + 1 by NAT_1:11;
then A14: k + 1 in dom g by A10, FINSEQ_3:25;
(len f) + 0 < (len f) + k by A1, A3;
then 0 < k ;
then 0 + 1 <= k by NAT_1:13;
then LSeg ((f ^' g),j) = LSeg (g,(k + 1)) by A3, A10, Th29;
then x in LSeg (g,(k + 1)) by A7, XBOOLE_0:def 4;
then x in (LSeg (g,(k + 1))) /\ (rng g) by A13, XBOOLE_0:def 4;
then ( x = g /. (k + 1) or x = g /. ((k + 1) + 1) ) by A11, TARSKI:def 2;
hence contradiction by A12, A5, A9, A8, A14, A6, PARTFUN2:10; :: thesis: verum