let S be TopSpace; :: thesis: for F being FinSequence of bool the carrier of S st ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) holds
union (rng F) is compact
let F be FinSequence of bool the carrier of S; :: thesis: ( ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) implies union (rng F) is compact )
assume A1: for i being Nat st i in Seg (len F) holds
F /. i is compact ; :: thesis: union (rng F) is compact
defpred S₁[ Nat] means for F being FinSequence of bool the carrier of S st len F = $1 & ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) holds
union (rng F) is compact ;
A2: S₁[ 0 ]

proof

let F be FinSequence of bool the carrier of S; :: thesis: ( len F = 0 & ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) implies union (rng F) is compact )
assume A3: ( len F = 0 & ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) ) ; :: thesis: union (rng F) is compact
dom F = {} by A3, FINSEQ_1:def 3;
then union (rng F) = {} by ZFMISC_1:2, RELAT_1:42;
hence union (rng F) is compact ; :: thesis: verum

end;

A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
let F be FinSequence of bool the carrier of S; :: thesis: ( len F = i + 1 & ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) implies union (rng F) is compact )
assume A6: ( len F = i + 1 & ( for i being Nat st i in Seg (len F) holds
F /. i is compact ) ) ; :: thesis: union (rng F) is compact
i + 1 in Seg (i + 1) by FINSEQ_1:4;
then A7: i + 1 in dom F by A6, FINSEQ_1:def 3;
A8: F = (F | i) ^ <*(F . (i + 1))*> by A6, FINSEQ_3:55;
A9: i <= i + 1 by NAT_1:11;
A10: len (F | i) = i by A6, FINSEQ_1:59, NAT_1:11;
then A11: dom (F | i) = Seg i by FINSEQ_1:def 3;
for k being Nat st k in Seg (len (F | i)) holds
(F | i) /. k is compact

proof

let k be Nat; :: thesis: ( k in Seg (len (F | i)) implies (F | i) /. k is compact )
assume A12: k in Seg (len (F | i)) ; :: thesis: (F | i) /. k is compact
then A13: k in Seg (i + 1) by A10, A9, FINSEQ_1:5, TARSKI:def 3;
then A14: k in dom F by A6, FINSEQ_1:def 3;
(F | i) /. k = (F | i) . k by A11, A12, A10, PARTFUN1:def 6
.= F . k by A12, A10, FUNCT_1:49
.= F /. k by PARTFUN1:def 6, A14 ;
hence (F | i) /. k is compact by A6, A13; :: thesis: verum

end;

then A15: union (rng (F | i)) is compact by A5, A10;
rng F = (rng (F | i)) \/ (rng <*(F . (i + 1))*>) by FINSEQ_1:31, A8
.= (rng (F | i)) \/ {(F . (i + 1))} by FINSEQ_1:39
.= (rng (F | i)) \/ {(F /. (i + 1))} by PARTFUN1:def 6, A7 ;
then A16: union (rng F) = (union (rng (F | i))) \/ (union {(F /. (i + 1))}) by ZFMISC_1:78
.= (union (rng (F | i))) \/ (F /. (i + 1)) by ZFMISC_1:25 ;
F /. (i + 1) is compact by A6, FINSEQ_1:4;
hence union (rng F) is compact by A16, A15, COMPTS_1:10; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A4);
hence union (rng F) is compact by A1; :: thesis: verum