let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Nat st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) implies f ^ g is s.n.c. )
assume that
A1: f is s.n.c. and
A2: g is s.n.c. and
A3: (L~ f) /\ (L~ g) = {} and
A4: for i being Nat st 1 <= i & i + 2 <= len f holds
LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) and
A5: for i being Nat st 2 <= i & i + 1 <= len g holds
LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ; :: according to XBOOLE_0:def 7 :: thesis: f ^ g is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) )
assume A6: i + 1 < j ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases ( i = 0 or j + 1 > len (f ^ g) or ( i <> 0 & j + 1 <= len (f ^ g) ) ) ;
suppose A7: ( i = 0 or j + 1 > len (f ^ g) ) ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
now :: thesis: ( ( i = 0 & LSeg ((f ^ g),i) = {} ) or ( j + 1 > len (f ^ g) & LSeg ((f ^ g),j) = {} ) )
per cases ( i = 0 or j + 1 > len (f ^ g) ) by A7;
case i = 0 ; :: thesis: LSeg ((f ^ g),i) = {}
hence LSeg ((f ^ g),i) = {} by TOPREAL1:def 3; :: thesis: verum
end;
case j + 1 > len (f ^ g) ; :: thesis: LSeg ((f ^ g),j) = {}
hence LSeg ((f ^ g),j) = {} by TOPREAL1:def 3; :: thesis: verum
end;
end;
end;
then (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} ;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; :: thesis: verum
end;
suppose that A8: i <> 0 and
A9: j + 1 <= len (f ^ g) ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
A10: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
i <= i + 1 by NAT_1:11;
then A11: i < j by A6, XXREAL_0:2;
A12: 1 <= i by A8, NAT_1:14;
now :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases ( j + 1 <= len f or j + 1 > len f ) ;
suppose A13: 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 A11, XXREAL_0:2;
then i < len f by A13, XXREAL_0:2;
then i + 1 <= len f by NAT_1:13;
then A14: LSeg ((f ^ g),i) = LSeg (f,i) by Th6;
LSeg ((f ^ g),j) = LSeg (f,j) by A13, Th6;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A1, A6, A14; :: thesis: verum
end;
suppose j + 1 > len f ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then A15: len f <= j by NAT_1:13;
then reconsider j9 = j - (len f) as Element of NAT by INT_1:5;
(j + 1) - (len f) <= len g by A9, A10, XREAL_1:20;
then A16: j9 + 1 <= len g ;
A17: (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 A18: i <= len f ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then A19: not f is empty by A12;
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)
not g is empty by A16;
then A21: LSeg ((f ^ g),i) = LSeg ((f /. (len f)),(g /. 1)) by A19, A20, Th8;
((len f) + 1) + 1 <= j by A6, A20, NAT_1:13;
then (len f) + (1 + 1) <= j ;
then A22: 1 + 1 <= j9 by XREAL_1:19;
then LSeg ((f ^ g),j) = LSeg (g,j9) by A17, Th7, XXREAL_0:2;
hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A5, A16, A22, A21; :: thesis: verum
end;
suppose i <> len f ; :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
then i < len f by A18, XXREAL_0:1;
then i + 1 <= len f by NAT_1:13;
then A23: LSeg ((f ^ g),i) = LSeg (f,i) by Th6;
now :: thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j)
per cases ( j = len f or j <> len f ) ;
suppose A24: 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 A25: i + (1 + 1) <= len f ;
not g is empty by A9, A10, A24, XREAL_1:6;
then A26: LSeg ((f ^ g),j) = LSeg ((f /. (len f)),(g /. 1)) by A19, A24, Th8;
thus LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A4, A8, A23, A25, A26, 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 A15, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by Th7;
then A27: LSeg ((f ^ g),j) c= L~ g by TOPREAL3:19;
LSeg ((f ^ g),i) c= L~ f by A23, TOPREAL3:19;
then (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} by A3, A27, XBOOLE_1:3, XBOOLE_1:27;
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 A28: 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 A15, XXREAL_0:1;
then (len f) + 1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then A29: LSeg ((f ^ g),((len f) + j9)) = LSeg (g,j9) by Th7;
reconsider i9 = i - (len f) as Element of NAT by A28, INT_1:5;
(len f) + 1 <= i by A28, NAT_1:13;
then 1 <= i9 by XREAL_1:19;
then A30: LSeg ((f ^ g),((len f) + i9)) = LSeg (g,i9) by Th7;
(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 A2, A30, A29; :: 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;