let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is unfolded & f is s.n.c. & f is one-to-one & g is unfolded & g is s.n.c. & g is one-to-one & f /. (len f) = g /. 1 & (L~ f) /\ (L~ g) = {(g /. 1)} implies f ^' g is s.n.c. )
assume that
A1: ( f is unfolded & f is s.n.c. & f is one-to-one ) and
A2: ( g is unfolded & g is s.n.c. & g is one-to-one ) and
A3: f /. (len f) = g /. 1 and
A4: (L~ f) /\ (L~ g) = {(g /. 1)} ; :: thesis: f ^' g is s.n.c.

now

let i, j be Nat; :: thesis: ( i + 1 < j implies LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) )
assume A5: i + 1 < j ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)
A6: i in NAT by ORDINAL1:def 12;
A7: j in NAT by ORDINAL1:def 12;

now

per cases ( j < len f or j >= len f ) ;

suppose A8: j < len f ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

then i + 1 < len f by A5, XXREAL_0:2;
then i < len f by NAT_1:13;
then A9: LSeg ((f ^' g),i) = LSeg (f,i) by A6, TOPREAL8:28;
LSeg ((f ^' g),j) = LSeg (f,j) by A7, A8, TOPREAL8:28;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A1, A5, A9, TOPREAL1:def 7; :: thesis: verum

end;

suppose j >= len f ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

then consider k being Nat such that
A10: j = (len f) + k by NAT_1:10;

A11: now

assume g is trivial ; :: thesis: contradiction
then len g < 2 by NAT_D:60;
then ( len g = 0 or len g = 1 ) by NAT_1:23;
then L~ g = {} by TOPREAL1:22;
hence contradiction by A4; :: thesis: verum

end;

reconsider k = k as Element of NAT by ORDINAL1:def 12;

A12: now

assume f is empty ; :: thesis: contradiction
then len f = 0 ;
then L~ f = {} by TOPREAL1:22;
hence contradiction by A4; :: thesis: verum

end;

now

per cases ( ( i >= 1 & j + 1 <= len (f ^' g) ) or j + 1 > len (f ^' g) or i < 1 ) ;

suppose A13: ( i >= 1 & j + 1 <= len (f ^' g) ) ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

then j + 1 < (len (f ^' g)) + 1 by NAT_1:13;
then (len f) + (k + 1) < (len f) + (len g) by A10, A11, GRAPH_2:13;
then A14: k + 1 < len g by XREAL_1:7;
then A15: LSeg ((f ^' g),((len f) + k)) = LSeg (g,(k + 1)) by A3, A12, A11, TOPREAL8:31;
then A16: LSeg ((f ^' g),j) c= L~ g by A10, TOPREAL3:19;

now

per cases ( i < len f or i >= len f ) ;

suppose A17: i < len f ; :: thesis: not LSeg ((f ^' g),i) meets LSeg ((f ^' g),j)

then A18: i + 1 <= len f by NAT_1:13;
i + 1 > 1 by A13, NAT_1:13;
then A19: i + 1 in dom f by A18, FINSEQ_3:25;
A20: len g >= 2 by A11, NAT_D:60;
A21: LSeg ((f ^' g),i) = LSeg (f,i) by A6, A17, TOPREAL8:28;
then LSeg ((f ^' g),i) c= L~ f by TOPREAL3:19;
then A22: (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) c= {(g /. 1)} by A4, A16, XBOOLE_1:27;
assume LSeg ((f ^' g),i) meets LSeg ((f ^' g),j) ; :: thesis: contradiction
then consider x being set such that
A23: x in LSeg ((f ^' g),i) and
A24: x in LSeg ((f ^' g),j) by XBOOLE_0:3;
x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) by A23, A24, XBOOLE_0:def 4;
then A25: x = g /. 1 by A22, TARSKI:def 1;
i in dom f by A13, A17, FINSEQ_3:25;
then (len f) + 0 < (len f) + k by A1, A3, A5, A10, A21, A23, A25, A19, GOBOARD2:2;
then k > 0 ;
then k + 1 > 0 + 1 by XREAL_1:6;
hence contradiction by A2, A10, A15, A24, A25, A20, JORDAN5B:30; :: thesis: verum

end;

suppose i >= len f ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

then consider l being Nat such that
A26: i = (len f) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
(len f) + (l + 1) < (len f) + k by A5, A10, A26;
then l + 1 < k by XREAL_1:7;
then A27: (l + 1) + 1 < k + 1 by XREAL_1:6;
then (l + 1) + 1 < len g by A14, XXREAL_0:2;
then l + 1 < len g by NAT_1:13;
then LSeg ((f ^' g),((len f) + l)) = LSeg (g,(l + 1)) by A3, A12, A11, TOPREAL8:31;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A2, A10, A15, A26, A27, TOPREAL1:def 7; :: thesis: verum

end;

end;

end;

hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) ; :: thesis: verum

end;

suppose j + 1 > len (f ^' g) ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

then LSeg ((f ^' g),j) = {} by TOPREAL1:def 3;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by XBOOLE_1:65; :: thesis: verum

end;

suppose i < 1 ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

then LSeg ((f ^' g),i) = {} by TOPREAL1:def 3;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) ; :: thesis: verum

end;

end;

end;

hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) ; :: thesis: verum

end;

hence f ^' g is s.n.c. by TOPREAL1:def 7; :: thesis: verum