let f be FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st f is s.n.c. holds
f /^ n is s.n.c.
let n be Nat; :: thesis: ( f is s.n.c. implies f /^ n is s.n.c. )
assume A1: f is s.n.c. ; :: thesis: f /^ n is s.n.c.
per cases ( n <= len f or n > len f ) ;
suppose A2: n <= len f ; :: thesis: f /^ n is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def 7 :: thesis: ( j <= i + 1 or LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) )
assume A3: i + 1 < j ; :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
now :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
per cases ( i = 0 or j + 1 > len (f /^ n) or ( i <> 0 & j + 1 <= len (f /^ n) ) ) ;
suppose A4: ( i = 0 or j + 1 > len (f /^ n) ) ; :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
now :: thesis: ( ( i = 0 & LSeg ((f /^ n),i) = {} ) or ( j + 1 > len (f /^ n) & LSeg ((f /^ n),j) = {} ) )
per cases ( i = 0 or j + 1 > len (f /^ n) ) by A4;
case i = 0 ; :: thesis: LSeg ((f /^ n),i) = {}
hence LSeg ((f /^ n),i) = {} by TOPREAL1:def 3; :: thesis: verum
end;
case j + 1 > len (f /^ n) ; :: thesis: LSeg ((f /^ n),j) = {}
hence LSeg ((f /^ n),j) = {} by TOPREAL1:def 3; :: thesis: verum
end;
end;
end;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ; :: thesis: verum
end;
suppose that A5: i <> 0 and
A6: j + 1 <= len (f /^ n) ; :: thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j)
A7: i <= j by A3, NAT_1:13;
1 <= i by A5, NAT_1:14;
then A8: 1 <= j by A7, XXREAL_0:2;
n + (i + 1) < n + j by A3, XREAL_1:6;
then (n + i) + 1 < n + j ;
then A9: LSeg (f,(n + i)) misses LSeg (f,(n + j)) by A1;
A10: len (f /^ n) = (len f) - n by A2, RFINSEQ:def 1;
j <= j + 1 by NAT_1:11;
then i + 1 < j + 1 by A3, XXREAL_0:2;
then i + 1 <= len (f /^ n) by A6, XXREAL_0:2;
then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = (LSeg (f,(n + i))) /\ (LSeg ((f /^ n),j)) by A5, A10, Th5, NAT_1:14
.= {} by A9, A6, A10, A8, Th5 ;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ; :: thesis: verum
end;
end;
end;
hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ; :: thesis: verum
end;
suppose n > len f ; :: thesis: f /^ n is s.n.c.
then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def 1;
then len (f /^ n) = 0 ;
hence f /^ n is s.n.c. by Th33; :: thesis: verum
end;
end;