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 Nat st 1 <= i & i + 2 <= len f holds
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being 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 Nat st 1 <= i & i + 2 <= len f holds
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} ) & ( for i being 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 Nat st 1 <= i & i + 2 <= len f holds
(LSeg (f,i)) /\ (LSeg ((f /. (len f)),(g /. 1))) = {} and
A5: for i being 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 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: for i being Nat st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) by A5;
A10: for i being Nat st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) by A4;
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 3;
then (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} ;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; :: 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:22;
i <= i + 1 by NAT_1:11;
then A13: i < j by A6, XXREAL_0:2;
now :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
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 A6, A15, TOPREAL1:def 7; :: 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 j9 = j - (len f) as Element of NAT by INT_1:5;
A17: (j + 1) - (len f) <= len g by A8, A12, XREAL_1:20;
then A18: j9 + 1 <= len g ;
A19: (len f) + j9 = j ;
now :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
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 :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases ( i = len f or i <> len f ) ;
suppose A21: i = len f ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
not g is empty by A18;
then A22: LSeg ((f ^ g),i) = LSeg ((f /. (len f)),(g /. 1)) by A21, SPPOL_2:8;
((len f) + 1) + 1 <= j by A6, A21, NAT_1:13;
then (len f) + (1 + 1) <= j ;
then A23: 1 + 1 <= j9 by XREAL_1:19;
then LSeg ((f ^ g),j) = LSeg (g,j9) by A19, SPPOL_2:7, XXREAL_0:2;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A9, A18, A23, A22; :: 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 A24: LSeg ((f ^ g),i) = LSeg (f,i) by SPPOL_2:6;
now :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases ( j = len f or j <> len f ) ;
suppose A25: 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 A26: i + (1 + 1) <= len f ;
not g is empty by A8, A12, A25, XREAL_1:6;
then LSeg ((f ^ g),j) = LSeg ((f /. (len f)),(g /. 1)) by A25, SPPOL_2:8;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A10, A11, A24, A26, NAT_1:14; :: thesis: verum
end;
suppose A27: j <> len f ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
A28: len f >= 2 by TOPREAL1:def 8;
A29: LSeg ((f ^ g),i) c= L~ f by A24, TOPREAL3:19;
len f < j by A16, A27, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then A30: 1 <= j9 by XREAL_1:19;
then A31: LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by SPPOL_2:7;
then LSeg ((f ^ g),j) c= L~ g by TOPREAL3:19;
then A32: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) c= {(f /. 1)} by A2, A29, XBOOLE_1:27;
now :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases ( (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} or (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {(f /. 1)} ) by A32, ZFMISC_1:33;
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) ; :: 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 A33: f /. 1 in (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) by TARSKI:def 1;
then A34: f /. 1 in LSeg ((f ^ g),i) by XBOOLE_0:def 4;
j9 < len g by A18, NAT_1:13;
then A35: j9 in dom g by A30, FINSEQ_3:25;
j9 + 1 >= 1 by NAT_1:11;
then A36: j9 + 1 in dom g by A17, FINSEQ_3:25;
f /. 1 in LSeg ((f ^ g),j) by A33, XBOOLE_0:def 4;
then j9 + 1 = len g by A1, A3, A31, A35, A36, GOBOARD2:2;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A7, A12, A24, A28, A34, JORDAN5B:30; :: 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 A37: 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 A16, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then A38: LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by SPPOL_2:7;
reconsider i9 = i - (len f) as Element of NAT by A37, INT_1:5;
(len f) + 1 <= i by A37, NAT_1:13;
then 1 <= i9 by XREAL_1:19;
then A39: LSeg ((f ^ g),((len f) + i9)) = LSeg (g,i9) by SPPOL_2:7;
(i + 1) - (len f) < j9 by A6, XREAL_1:9;
then i9 + 1 < j9 ;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A1, A39, A38, TOPREAL1:def 7; :: 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;