let f be S-Sequence_in_R2; :: thesis: for g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds
(LSeg f,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds
(LSeg g,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ) holds
f ^ g is s.c.c.
let g be FinSequence of (TOP-REAL 2); :: thesis: ( g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds
(LSeg f,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds
(LSeg g,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ) implies f ^ g is s.c.c. )
assume that
A1: ( g is unfolded & g is s.n.c. & g is one-to-one ) and
A2: (L~ f) /\ (L~ g) = {(f /. 1)} and
A3: f /. 1 = g /. (len g) and
A4: for i being Element of NAT st 1 <= i & i + 2 <= len f holds
(LSeg f,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} and
A5: for i being Element of NAT st 2 <= i & i + 1 <= len g holds
(LSeg g,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ; :: thesis: f ^ g is s.c.c.

A6: now

let i be Element of NAT ; :: thesis: ( 1 <= i & i + 2 <= len f implies LSeg f,i misses LSeg (f /. (len f)),(g /. 1) )
assume ( 1 <= i & i + 2 <= len f ) ; :: thesis: LSeg f,i misses LSeg (f /. (len f)),(g /. 1)
then (LSeg f,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} by A4;
hence LSeg f,i misses LSeg (f /. (len f)),(g /. 1) by XBOOLE_0:def 7; :: thesis: verum

end;

A7: now

let i be Element of NAT ; :: thesis: ( 2 <= i & i + 1 <= len g implies LSeg g,i misses LSeg (f /. (len f)),(g /. 1) )
assume ( 2 <= i & i + 1 <= len g ) ; :: thesis: LSeg g,i misses LSeg (f /. (len f)),(g /. 1)
then (LSeg g,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} by A5;
hence LSeg g,i misses LSeg (f /. (len f)),(g /. 1) by XBOOLE_0:def 7; :: thesis: verum

end;

let i, j be Element of NAT ; :: according to GOBOARD5:def 4 :: thesis: ( j <= i + 1 or ( ( i <= 1 or len (f ^ g) <= j ) & len (f ^ g) <= j + 1 ) or LSeg (f ^ g),i misses LSeg (f ^ g),j )
assume that
A8: i + 1 < j and
A9: ( ( i > 1 & j < len (f ^ g) ) or j + 1 < len (f ^ g) ) ; :: thesis: LSeg (f ^ g),i misses LSeg (f ^ g),j
A10: j + 1 <= len (f ^ g) by A9, NAT_1:13;

per cases ( i = 0 or i <> 0 ) ;

suppose i = 0 ; :: thesis: LSeg (f ^ g),i misses LSeg (f ^ g),j

then LSeg (f ^ g),i = {} by TOPREAL1:def 5;
then (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) = {} ;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose A11: i <> 0 ; :: thesis: LSeg (f ^ g),i misses LSeg (f ^ g),j

A12: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
i <= i + 1 by NAT_1:11;
then A13: i < j by A8, XXREAL_0:2;

now

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

suppose A14: j + 1 <= len f ; :: thesis: LSeg (f ^ g),i misses LSeg (f ^ g),j

j <= j + 1 by NAT_1:11;
then i < j + 1 by A13, XXREAL_0:2;
then i < len f by A14, XXREAL_0:2;
then i + 1 <= len f by NAT_1:13;
then A15: LSeg (f ^ g),i = LSeg f,i by SPPOL_2:6;
LSeg (f ^ g),j = LSeg f,j by A14, SPPOL_2:6;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A8, A15, TOPREAL1:def 9; :: thesis: verum

end;

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

then A16: len f <= j by NAT_1:13;
then reconsider j' = j - (len f) as Element of NAT by INT_1:18;
A17: (len f) + j' = j ;
A18: (j + 1) - (len f) <= len g by A10, A12, XREAL_1:22;
then A19: j' + 1 <= len g ;

now

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

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

now

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

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

then ((len f) + 1) + 1 <= j by A8, NAT_1:13;
then (len f) + (1 + 1) <= j ;
then A22: 1 + 1 <= j' by XREAL_1:21;
A24: LSeg (f ^ g),j = LSeg g,j' by A17, A22, SPPOL_2:7, XXREAL_0:2;
not g is empty by A19;
then LSeg (f ^ g),i = LSeg (f /. (len f)),(g /. 1) by A21, SPPOL_2:8;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A7, A19, A22, A24; :: thesis: verum

end;

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

then i < len f by A20, XXREAL_0:1;
then i + 1 <= len f by NAT_1:13;
then A25: LSeg (f ^ g),i = LSeg f,i by SPPOL_2:6;

now

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

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

then (i + 1) + 1 <= len f by A8, NAT_1:13;
then A27: i + (1 + 1) <= len f ;
1 <= len g by A10, A12, A26, XREAL_1:8;
then not g is empty ;
then LSeg (f ^ g),j = LSeg (f /. (len f)),(g /. 1) by A26, SPPOL_2:8;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A6, A11, A25, A27, NAT_1:14; :: thesis: verum

end;

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

then len f < j by A16, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then A28: 1 <= j' by XREAL_1:21;
then A29: LSeg (f ^ g),((len f) + j') = LSeg g,j' by SPPOL_2:7;
then A30: LSeg (f ^ g),j c= L~ g by TOPREAL3:26;
LSeg (f ^ g),i c= L~ f by A25, TOPREAL3:26;
then A31: (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) c= {(f /. 1)} by A2, A30, XBOOLE_1:27;
A32: len f >= 2 by TOPREAL1:def 10;

now

per cases ( (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) = {} or (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) = {(f /. 1)} ) by A31, ZFMISC_1:39;

suppose (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) = {} ; :: thesis: LSeg (f ^ g),i misses LSeg (f ^ g),j

hence LSeg (f ^ g),i misses LSeg (f ^ g),j by XBOOLE_0:def 7; :: thesis: verum

end;

suppose (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) = {(f /. 1)} ; :: thesis: LSeg (f ^ g),i misses LSeg (f ^ g),j

then f /. 1 in (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) by TARSKI:def 1;
then A33: ( f /. 1 in LSeg (f ^ g),i & f /. 1 in LSeg (f ^ g),j ) by XBOOLE_0:def 4;
( j' + 1 >= 1 & j' < len g ) by A19, NAT_1:11, NAT_1:13;
then ( j' in dom g & j' + 1 in dom g ) by A18, A28, FINSEQ_3:27;
then j' + 1 = len g by A1, A3, A29, A33, GOBOARD2:7;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A9, A12, A25, A32, A33, JORDAN5B:33; :: 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;

end;

end;

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

end;

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

then reconsider i' = i - (len f) as Element of NAT by INT_1:18;
(len f) + 1 <= i by A34, NAT_1:13;
then 1 <= i' by XREAL_1:21;
then A35: LSeg (f ^ g),((len f) + i') = LSeg g,i' by SPPOL_2:7;
(i + 1) - (len f) < j' by A8, XREAL_1:11;
then A36: i' + 1 < j' ;
j <> len f by A8, A34, NAT_1:13;
then len f < j by A16, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j' by XREAL_1:21;
then LSeg (f ^ g),((len f) + j') = LSeg g,j' by SPPOL_2:7;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A1, A35, A36, TOPREAL1:def 9; :: 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;

end;