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
proof
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;
then union (rng U) in the topology of T by PRE_TOPC:def 1;
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