let T be non empty TopSpace; :: thesis: for FX being Subset-Family of T st FX is finite holds
Cl (union FX) = union (clf FX)
let FX be Subset-Family of T; :: thesis: ( FX is finite implies Cl (union FX) = union (clf FX) )
assume FX is finite ; :: thesis: Cl (union FX) = union (clf FX)
then consider p being FinSequence such that
A1: rng p = FX by FINSEQ_1:52;
consider n being Nat such that
A2: dom p = Seg n by FINSEQ_1:def 2;
defpred S₁[ Nat] means for GX being Subset-Family of T st GX = p .: (Seg $1) & $1 <= n & 1 <= n holds
Cl (union GX) = union (clf GX);
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: for GX being Subset-Family of T st GX = p .: (Seg k) & k <= n & 1 <= n holds
Cl (union GX) = union (clf GX) ; :: thesis: S₁[k + 1]
let GX be Subset-Family of T; :: thesis: ( GX = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies Cl (union GX) = union (clf GX) )
assume A5: GX = p .: (Seg (k + 1)) ; :: thesis: ( not k + 1 <= n or not 1 <= n or Cl (union GX) = union (clf GX) )
assume that
A6: k + 1 <= n and
A7: 1 <= n ; :: thesis: Cl (union GX) = union (clf GX)

now :: thesis: Cl (union GX) = union (clf GX)

reconsider G2 = Im (p,(k + 1)) as Subset-Family of T by A1, RELAT_1:111, TOPS_2:2;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A1, RELAT_1:111, TOPS_2:2;
k + 1 <= n + 1 by A6, NAT_1:12;
then A8: k <= n by XREAL_1:6;
0 + 1 = 1 ;
then 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom p by A2, A6, FINSEQ_1:1;
then A9: G2 = {(p . (k + 1))} by FUNCT_1:59;
then union G2 = p . (k + 1) by ZFMISC_1:25;
then reconsider G3 = p . (k + 1) as Subset of T ;
A10: union (clf G2) = union {(Cl G3)} by A9, Th13
.= Cl G3 by ZFMISC_1:25
.= Cl (union G2) by A9, ZFMISC_1:25 ;
A11: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ;
then Cl (union GX) = Cl ((union G1) \/ (union G2)) by A5, ZFMISC_1:78
.= (Cl (union G1)) \/ (Cl (union G2)) by PRE_TOPC:20 ;
then Cl (union GX) = (union (clf G1)) \/ (union (clf G2)) by A4, A7, A10, A8;
then Cl (union GX) = union ((clf G1) \/ (clf G2)) by ZFMISC_1:78;
hence Cl (union GX) = union (clf GX) by A5, A11, Th15; :: thesis: verum

end;

hence Cl (union GX) = union (clf GX) ; :: thesis: verum

end;

A12: S₁[ 0 ]

proof

let GX be Subset-Family of T; :: thesis: ( GX = p .: (Seg 0) & 0 <= n & 1 <= n implies Cl (union GX) = union (clf GX) )
assume that
A13: GX = p .: (Seg 0) and
0 <= n and
1 <= n ; :: thesis: Cl (union GX) = union (clf GX)
union GX = {} T by A13, ZFMISC_1:2;
then Cl (union GX) = {} T by PRE_TOPC:22;
hence Cl (union GX) = union (clf GX) by A13, Th12, ZFMISC_1:2; :: thesis: verum

end;

A14: for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A3);

A15: now :: thesis: ( 1 <= n implies Cl (union FX) = union (clf FX) )

assume A16: 1 <= n ; :: thesis: Cl (union FX) = union (clf FX)
FX = p .: (Seg n) by A1, A2, RELAT_1:113;
hence Cl (union FX) = union (clf FX) by A14, A16; :: thesis: verum

end;

A17: now :: thesis: ( n = 0 implies Cl (union FX) = union (clf FX) )

assume n = 0 ; :: thesis: Cl (union FX) = union (clf FX)
then Seg n = {} ;
then A18: FX = p .: {} by A1, A2, RELAT_1:113;
then union FX = {} T by ZFMISC_1:2;
then Cl (union FX) = {} T by PRE_TOPC:22;
hence Cl (union FX) = union (clf FX) by A18, Th12, ZFMISC_1:2; :: thesis: verum

end;

now :: thesis: ( n <> 0 implies 1 <= n )

A19: 1 = 0 + 1 ;
assume n <> 0 ; :: thesis: 1 <= n
hence 1 <= n by A19, NAT_1:13; :: thesis: verum

end;

hence Cl (union FX) = union (clf FX) by A15, A17; :: thesis: verum