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: 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
A4: GX = p .: (Seg 0 ) and
( 0 <= n & 1 <= n ) ; :: thesis: Cl (union GX) = union (clf GX)
union GX = {} T by A4, 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 A4, Th15, FINSEQ_1:4, RELAT_1:149, ZFMISC_1:2; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: 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 A7: GX = p .: (Seg (k + 1)) ; :: thesis: ( not k + 1 <= n or not 1 <= n or Cl (union GX) = union (clf GX) )
assume A8: ( k + 1 <= n & 1 <= n ) ; :: thesis: Cl (union GX) = union (clf GX)

now

A9: p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:11
.= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:153 ;
reconsider G1 = p .: (Seg k) as Subset-Family of T by A1, RELAT_1:144, TOPS_2:3;
reconsider G2 = Im p,(k + 1) as Subset-Family of T by A1, RELAT_1:144, TOPS_2:3;
( 0 <= k & 0 + 1 = 1 ) ;
then ( 1 <= k + 1 & k + 1 <= n ) by A8, XREAL_1:9;
then A10: k + 1 in dom p by A2, FINSEQ_1:3;
A11: Cl (union GX) = Cl ((union G1) \/ (union G2)) by A7, A9, ZFMISC_1:96
.= (Cl (union G1)) \/ (Cl (union G2)) by PRE_TOPC:50 ;
A12: G2 = {(p . (k + 1))} by A10, FUNCT_1:117;
then ( union G2 = p . (k + 1) & p . (k + 1) in FX ) by A1, A10, FUNCT_1:def 5, ZFMISC_1:31;
then reconsider G3 = p . (k + 1) as Subset of T ;
A13: union (clf G2) = union {(Cl G3)} by A12, Th16
.= Cl G3 by ZFMISC_1:31
.= Cl (union G2) by A12, ZFMISC_1:31 ;
k + 1 <= n + 1 by A8, NAT_1:12;
then k <= n by XREAL_1:8;
then Cl (union GX) = (union (clf G1)) \/ (union (clf G2)) by A6, A8, A11, A13;
then Cl (union GX) = union ((clf G1) \/ (clf G2)) by ZFMISC_1:96;
hence Cl (union GX) = union (clf GX) by A7, A9, Th18; :: thesis: verum

end;

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

end;

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

A15: now

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

end;

A16: now

assume n = 0 ; :: thesis: Cl (union FX) = union (clf FX)
then A17: 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 A17, Th15, RELAT_1:149, ZFMISC_1:2; :: thesis: verum

end;

now

assume n <> 0 ; :: thesis: 1 <= n
then ( 0 < n & 1 = 0 + 1 ) ;
hence 1 <= n by NAT_1:13; :: thesis: verum

end;

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