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:73;
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

reconsider G2 = Im p,(k + 1) as Subset-Family of T by A1, RELAT_1:144, TOPS_2:3;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A1, RELAT_1:144, TOPS_2:3;
k + 1 <= n + 1 by A6, NAT_1:12;
then A8: k <= n by XREAL_1:8;
0 + 1 = 1 ;
then 1 <= k + 1 by XREAL_1:9;
then k + 1 in dom p by A2, A6, FINSEQ_1:3;
then A9: G2 = {(p . (k + 1))} by FUNCT_1:117;
then union G2 = p . (k + 1) by ZFMISC_1:31;
then reconsider G3 = p . (k + 1) as Subset of T ;
A10: union (clf G2) = union {(Cl G3)} by A9, Th16
.= Cl G3 by ZFMISC_1:31
.= Cl (union G2) by A9, ZFMISC_1:31 ;
A11: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:11
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:153 ;
then Cl (union GX) = Cl ((union G1) \/ (union G2)) by A5, ZFMISC_1:96
.= (Cl (union G1)) \/ (Cl (union G2)) by PRE_TOPC:50 ;
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:96;
hence Cl (union GX) = union (clf GX) by A5, A11, Th18; :: 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, FINSEQ_1:4, RELAT_1:149, ZFMISC_1:2;
then Cl (union GX) = {} T by PRE_TOPC:52;
hence Cl (union GX) = union (clf GX) by A13, Th15, FINSEQ_1:4, RELAT_1:149, ZFMISC_1:2; :: thesis: verum

end;

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

A15: now

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

end;

A17: now

assume n = 0 ; :: thesis: Cl (union FX) = union (clf FX)
then Seg n = {} ;
then A18: FX = p .: {} by A1, A2, FINSEQ_1:4, RELAT_1:146;
then union FX = {} T by RELAT_1:149, ZFMISC_1:2;
then Cl (union FX) = {} T by PRE_TOPC:52;
hence Cl (union FX) = union (clf FX) by A18, Th15, RELAT_1:149, ZFMISC_1:2; :: thesis: verum

end;

now

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