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;
A11: 1 <= i by A8, NAT_1:14;
i <= i + 1 by NAT_1:11;
then A12: i < j by A6, XXREAL_0:2;

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 A12, 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 j' = j - (len f) as Element of NAT by INT_1:18;
A16: (len f) + j' = j ;
(j + 1) - (len f) <= len g by A9, A10, XREAL_1:22;
then A17: j' + 1 <= len g ;

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 A11;

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

then ((len f) + 1) + 1 <= j by A6, NAT_1:13;
then (len f) + (1 + 1) <= j ;
then A21: 1 + 1 <= j' by XREAL_1:21;
A23: LSeg (f ^ g),j = LSeg g,j' by A16, A21, Th7, XXREAL_0:2;
not g is empty by A17;
then LSeg (f ^ g),i = LSeg (f /. (len f)),(g /. 1) by A19, A20, Th8;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A5, A17, A21, A23; :: 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 A24: LSeg (f ^ g),i = LSeg f,i by Th6;

now

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 ;
A27: ( i in NAT & j in NAT ) by ORDINAL1:def 13;
1 <= len g by A9, A10, A25, XREAL_1:8;
then not g is empty ;
then LSeg (f ^ g),j = LSeg (f /. (len f)),(g /. 1) by A19, A25, Th8;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A4, A8, A24, A26, 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 A15, 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 Th7;
then A28: LSeg (f ^ g),j c= L~ g by TOPREAL3:26;
LSeg (f ^ g),i c= L~ f by A24, TOPREAL3:26;
then (LSeg (f ^ g),i) /\ (LSeg (f ^ g),j) = {} by A3, A28, 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 A29: 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 A29, NAT_1:13;
then 1 <= i' by XREAL_1:21;
then A30: LSeg (f ^ g),((len f) + i') = LSeg g,i' by Th7;
(i + 1) - (len f) < j' by A6, XREAL_1:11;
then A31: i' + 1 < j' ;
j <> len f by A6, A29, NAT_1:13;
then len f < j by A15, 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 Th7;
hence LSeg (f ^ g),i misses LSeg (f ^ g),j by A2, A30, A31, 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;