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