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 Element of NAT st 1 <= i & i + 2 <= len f holds
LSeg f,i misses LSeg (f /. (len f)),(g /. 1) ) & ( for i being Element of 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 Element of NAT st 1 <= i & i + 2 <= len f holds
LSeg f,i misses 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 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 9 :: 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

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 5; :: thesis: verum

end;

case j + 1 > len (f ^ g) ; :: thesis: LSeg (f ^ g),j = {}

hence LSeg (f ^ g),j = {} by TOPREAL1:def 5; :: thesis: verum

end;

end;

end;

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 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:35;
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

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, TOPREAL1:def 9; :: 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:18;
(j + 1) - (len f) <= len g by A9, A10, XREAL_1:22;
then A16: j9 + 1 <= len g ;
A17: (len f) + j9 = j ;

now

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

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:21;
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

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:8;
then A26: LSeg (f ^ g),j = LSeg (f /. (len f)),(g /. 1) by A19, A24, Th8;
i in NAT by ORDINAL1:def 13;
hence 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:21;
then LSeg (f ^ g),((len f) + j9) = LSeg g,j9 by Th7;
then A27: LSeg (f ^ g),j c= L~ g by TOPREAL3:26;
LSeg (f ^ g),i c= L~ f by A23, TOPREAL3:26;
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 by XBOOLE_0: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;

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:21;
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:18;
(len f) + 1 <= i by A28, NAT_1:13;
then 1 <= i9 by XREAL_1:21;
then A30: LSeg (f ^ g),((len f) + i9) = LSeg g,i9 by Th7;
(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 A2, A30, A29, 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;