let F be FinSequence of bool REAL; :: thesis: for k being Nat st ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st 1 <= n & n < len F holds
union (rng (F | n)) meets F . (n + 1) ) holds
union (rng (F | k)) is open_interval Subset of REAL
let k be Nat; :: thesis: ( ( for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL ) & ( for n being Nat st 1 <= n & n < len F holds
union (rng (F | n)) meets F . (n + 1) ) implies union (rng (F | k)) is open_interval Subset of REAL )
assume that
A1: for n being Nat st n in dom F holds
F . n is open_interval Subset of REAL and
A2: for n being Nat st 1 <= n & n < len F holds
union (rng (F | n)) meets F . (n + 1) ; :: thesis: union (rng (F | k)) is open_interval Subset of REAL
A3: now :: thesis: for k being Nat st k = 0 holds
union (rng (F | k)) is open_interval Subset of REAL
let k be Nat; :: thesis: ( k = 0 implies union (rng (F | k)) is open_interval Subset of REAL )
assume k = 0 ; :: thesis: union (rng (F | k)) is open_interval Subset of REAL
then union (rng (F | k)) = {} by ZFMISC_1:2;
hence union (rng (F | k)) is open_interval Subset of REAL ; :: thesis: verum
end;
defpred S1[ Nat] means union (rng (F | $1)) is open_interval Subset of REAL;
A4: S1[ 0 ] by A3;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
per cases ( ( 1 <= k + 1 & k + 1 <= len F ) or k + 1 < 1 or len F < k + 1 ) ;
suppose A7: ( 1 <= k + 1 & k + 1 <= len F ) ; :: thesis: S1[k + 1]
then A8: k < len F by NAT_1:13;
A9: 1 <= len F by A7, XXREAL_0:2;
A10: F . (k + 1) is open_interval Subset of REAL by A1, A7, FINSEQ_3:25;
A11: F <> {} by A7;
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: S1[k + 1]
then F | (k + 1) = <*(F . 1)*> by A11, FINSEQ_5:20;
then rng (F | (k + 1)) = {(F . 1)} by FINSEQ_1:38;
hence union (rng (F | (k + 1))) is open_interval Subset of REAL by A1, A9, FINSEQ_3:25; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: S1[k + 1]
then A12: 1 <= k by NAT_1:14;
F | (k + 1) = (F | k) ^ <*(F . (k + 1))*> by A7, NAT_1:13, FINSEQ_5:83;
then rng (F | (k + 1)) = (rng (F | k)) \/ (rng <*(F . (k + 1))*>) by FINSEQ_1:31
.= (rng (F | k)) \/ {(F . (k + 1))} by FINSEQ_1:38 ;
then union (rng (F | (k + 1))) = (union (rng (F | k))) \/ (union {(F . (k + 1))}) by ZFMISC_1:78;
hence union (rng (F | (k + 1))) is open_interval Subset of REAL by A12, A2, A6, A8, A10, Th2; :: thesis: verum
end;
end;
end;
suppose ( k + 1 < 1 or len F < k + 1 ) ; :: thesis: S1[k + 1]
then ( k + 1 = 0 or ( F | (k + 1) = F & len F <= k ) ) by NAT_1:13, NAT_1:14, FINSEQ_1:58;
hence union (rng (F | (k + 1))) is open_interval Subset of REAL by A6, FINSEQ_1:58; :: thesis: verum
end;
end;
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A5);
 hence union (rng (F | k)) is open_interval Subset of REAL ; :: thesis: verum