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 & j in NAT ) by ORDINAL1:def 13;
now
per cases ( j < len f or j >= len f ) ;
suppose A7: j < len f ; :: thesis: LSeg (f ^' g),i misses LSeg (f ^' g),j
then A8: LSeg (f ^' g),j = LSeg f,j by A6, TOPREAL8:28;
i + 1 < len f by A5, A7, XXREAL_0:2;
then i < len f by NAT_1:13;
then LSeg (f ^' g),i = LSeg f,i by A6, TOPREAL8:28;
hence LSeg (f ^' g),i misses LSeg (f ^' g),j by A1, A5, A8, TOPREAL1:def 9; :: thesis: verum
end;
suppose j >= len f ; :: thesis: LSeg (f ^' g),i misses LSeg (f ^' g),j
then consider k being Nat such that
A9: j = (len f) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
now
per cases ( ( i >= 1 & j + 1 <= len (f ^' g) ) or j + 1 > len (f ^' g) or i < 1 ) ;
suppose A12: ( 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 A9, A11, GRAPH_2:13;
then A13: k + 1 < len g by XREAL_1:9;
then A14: LSeg (f ^' g),((len f) + k) = LSeg g,(k + 1) by A3, A10, A11, TOPREAL8:31;
then A15: LSeg (f ^' g),j c= L~ g by A9, TOPREAL3:26;
now
per cases ( i < len f or i >= len f ) ;
suppose A16: i < len f ; :: thesis: not LSeg (f ^' g),i meets LSeg (f ^' g),j
then A17: LSeg (f ^' g),i = LSeg f,i by A6, TOPREAL8:28;
then LSeg (f ^' g),i c= L~ f by TOPREAL3:26;
then A18: (LSeg (f ^' g),i) /\ (LSeg (f ^' g),j) c= {(g /. 1)} by A4, A15, XBOOLE_1:27;
assume LSeg (f ^' g),i meets LSeg (f ^' g),j ; :: thesis: contradiction
then consider x being set such that
A19: x in LSeg (f ^' g),i and
A20: x in LSeg (f ^' g),j by XBOOLE_0:3;
x in (LSeg (f ^' g),i) /\ (LSeg (f ^' g),j) by A19, A20, XBOOLE_0:def 4;
then A21: x = g /. 1 by A18, TARSKI:def 1;
A22: i in dom f by A12, A16, FINSEQ_3:27;
( i + 1 > 1 & i + 1 <= len f ) by A12, A16, NAT_1:13;
then i + 1 in dom f by FINSEQ_3:27;
then (len f) + 0 < (len f) + k by A1, A3, A5, A9, A17, A19, A21, A22, GOBOARD2:7;
then k > 0 ;
then A23: k + 1 > 0 + 1 by XREAL_1:8;
len g >= 2 by A11, REALSET1:13;
hence contradiction by A2, A9, A14, A20, A21, A23, JORDAN5B:33; :: 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 Element of NAT by ORDINAL1:def 13;
(len f) + (l + 1) < (len f) + k by A5, A9, A24;
then l + 1 < k by XREAL_1:9;
then A25: (l + 1) + 1 < k + 1 by XREAL_1:8;
then (l + 1) + 1 < len g by A13, 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, A11, TOPREAL8:31;
hence LSeg (f ^' g),i misses LSeg (f ^' g),j by A2, A9, A14, A24, A25, TOPREAL1:def 9; :: 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 5;
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 5;
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 9; :: thesis: verum