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 :: thesis: for i, j being Nat st i + 1 < j holds
LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

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)

now :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

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

suppose A6: 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 A7: LSeg ((f ^' g),i) = LSeg (f,i) by TOPREAL8:28;
LSeg ((f ^' g),j) = LSeg (f,j) by A6, TOPREAL8:28;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A1, A5, A7, 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
A8: j = (len f) + k by NAT_1:10;

A9: now :: thesis: not g is trivial

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 Nat ;

A10: now :: thesis: not f is empty

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

end;

now :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)

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

suppose A11: ( 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 A8, A9, FINSEQ_6:139;
then A12: k + 1 < len g by XREAL_1:7;
then A13: LSeg ((f ^' g),((len f) + k)) = LSeg (g,(k + 1)) by A3, A10, A9, TOPREAL8:31;
then A14: LSeg ((f ^' g),j) c= L~ g by A8, TOPREAL3:19;

now :: thesis: not LSeg ((f ^' g),i) meets LSeg ((f ^' g),j)

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

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

then A16: i + 1 <= len f by NAT_1:13;
i + 1 > 1 by A11, NAT_1:13;
then A17: i + 1 in dom f by A16, FINSEQ_3:25;
A18: len g >= 2 by A9, NAT_D:60;
A19: LSeg ((f ^' g),i) = LSeg (f,i) by A15, TOPREAL8:28;
then LSeg ((f ^' g),i) c= L~ f by TOPREAL3:19;
then A20: (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) c= {(g /. 1)} by A4, A14, XBOOLE_1:27;
assume LSeg ((f ^' g),i) meets LSeg ((f ^' g),j) ; :: thesis: contradiction
then consider x being object such that
A21: x in LSeg ((f ^' g),i) and
A22: x in LSeg ((f ^' g),j) by XBOOLE_0:3;
x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) by A21, A22, XBOOLE_0:def 4;
then A23: x = g /. 1 by A20, TARSKI:def 1;
i in dom f by A11, A15, FINSEQ_3:25;
then (len f) + 0 < (len f) + k by A1, A3, A5, A8, A19, A21, A23, A17, GOBOARD2:2;
then k > 0 ;
then k + 1 > 0 + 1 by XREAL_1:6;
hence contradiction by A2, A8, A13, A22, A23, A18, 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
A24: i = (len f) + l by NAT_1:10;
reconsider l = l as Nat ;
(len f) + (l + 1) < (len f) + k by A5, A8, A24;
then l + 1 < k by XREAL_1:7;
then A25: (l + 1) + 1 < k + 1 by XREAL_1:6;
then (l + 1) + 1 < len g by A12, 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, A10, A9, TOPREAL8:31;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A2, A8, A13, A24, A25, 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) ; :: 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) ; :: 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