let T be non empty TopSpace; :: thesis: for U being sequence of (bool the carrier of T) st ( for n being Element of NAT holds U . n is open ) holds

Union U is open

let U be sequence of (bool the carrier of T); :: thesis: ( ( for n being Element of NAT holds U . n is open ) implies Union U is open )

assume A1: for n being Element of NAT holds U . n is open ; :: thesis: Union U is open

rng U c= the topology of T

then Union U in the topology of T by CARD_3:def 4;

hence Union U is open by PRE_TOPC:def 2; :: thesis: verum

Union U is open

let U be sequence of (bool the carrier of T); :: thesis: ( ( for n being Element of NAT holds U . n is open ) implies Union U is open )

assume A1: for n being Element of NAT holds U . n is open ; :: thesis: Union U is open

rng U c= the topology of T

proof

then
union (rng U) in the topology of T
by PRE_TOPC:def 1;
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng U or u in the topology of T )

assume u in rng U ; :: thesis: u in the topology of T

then consider k being object such that

A2: k in dom U and

A3: u = U . k by FUNCT_1:def 3;

reconsider k = k as Element of NAT by A2;

U . k is open by A1;

hence u in the topology of T by A3, PRE_TOPC:def 2; :: thesis: verum

end;assume u in rng U ; :: thesis: u in the topology of T

then consider k being object such that

A2: k in dom U and

A3: u = U . k by FUNCT_1:def 3;

reconsider k = k as Element of NAT by A2;

U . k is open by A1;

hence u in the topology of T by A3, PRE_TOPC:def 2; :: thesis: verum

then Union U in the topology of T by CARD_3:def 4;

hence Union U is open by PRE_TOPC:def 2; :: thesis: verum