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.
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
A6: i + 1 < j and
A7: ( ( i > 1 & j < len (f ^ g) ) or j + 1 < len (f ^ g) ) ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
A8: j + 1 <= len (f ^ g) by A7, NAT_1:13;

A9: 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 that
A10: 2 <= i and
A11: i + 1 <= len g ; :: thesis: LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1))
(LSeg (g,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} by A5, A10, A11;
hence LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) by XBOOLE_0:def 7; :: thesis: verum

end;

A12: 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 that
A13: 1 <= i and
A14: i + 2 <= len f ; :: thesis: LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1))
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} by A4, A13, A14;
hence LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) by XBOOLE_0:def 7; :: thesis: verum

end;

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 A15: i <> 0 ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)

A16: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
i <= i + 1 by NAT_1:11;
then A17: i < j by A6, XXREAL_0:2;

now

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

suppose A18: 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 A17, XXREAL_0:2;
then i < len f by A18, XXREAL_0:2;
then i + 1 <= len f by NAT_1:13;
then A19: LSeg ((f ^ g),i) = LSeg (f,i) by SPPOL_2:6;
LSeg ((f ^ g),j) = LSeg (f,j) by A18, SPPOL_2:6;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A6, A19, TOPREAL1:def 9; :: thesis: verum

end;

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

then A20: len f <= j by NAT_1:13;
then reconsider j9 = j - (len f) as Element of NAT by INT_1:18;
A21: (j + 1) - (len f) <= len g by A8, A16, XREAL_1:22;
then A22: j9 + 1 <= len g ;
A23: (len f) + j9 = j ;

now

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

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

now

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

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

not g is empty by A22;
then A26: LSeg ((f ^ g),i) = LSeg ((f /. (len f)),(g /. 1)) by A25, SPPOL_2:8;
((len f) + 1) + 1 <= j by A6, A25, NAT_1:13;
then (len f) + (1 + 1) <= j ;
then A27: 1 + 1 <= j9 by XREAL_1:21;
then LSeg ((f ^ g),j) = LSeg (g,j9) by A23, SPPOL_2:7, XXREAL_0:2;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A9, A22, A27, A26; :: thesis: verum

end;

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

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

now

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

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

then (i + 1) + 1 <= len f by A6, NAT_1:13;
then A30: i + (1 + 1) <= len f ;
not g is empty by A8, A16, A29, XREAL_1:8;
then LSeg ((f ^ g),j) = LSeg ((f /. (len f)),(g /. 1)) by A29, SPPOL_2:8;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A12, A15, A28, A30, NAT_1:14; :: thesis: verum

end;

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

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

now

per cases ( (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} or (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {(f /. 1)} ) by A36, 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 A37: f /. 1 in (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) by TARSKI:def 1;
then A38: f /. 1 in LSeg ((f ^ g),i) by XBOOLE_0:def 4;
j9 < len g by A22, NAT_1:13;
then A39: j9 in dom g by A34, FINSEQ_3:27;
j9 + 1 >= 1 by NAT_1:11;
then A40: j9 + 1 in dom g by A21, FINSEQ_3:27;
f /. 1 in LSeg ((f ^ g),j) by A37, XBOOLE_0:def 4;
then j9 + 1 = len g by A1, A3, A35, A39, A40, GOBOARD2:7;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A7, A16, A28, A32, A38, 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 A41: i > len f ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)

then j <> len f by A6, NAT_1:13;
then len f < j by A20, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:21;
then A42: LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by SPPOL_2:7;
reconsider i9 = i - (len f) as Element of NAT by A41, INT_1:18;
(len f) + 1 <= i by A41, NAT_1:13;
then 1 <= i9 by XREAL_1:21;
then A43: LSeg ((f ^ g),((len f) + i9)) = LSeg (g,i9) by SPPOL_2:7;
(i + 1) - (len f) < j9 by A6, XREAL_1:11;
then i9 + 1 < j9 ;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A1, A43, A42, 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;