let I be 1 -element set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of I
for i being Element of I
for P being Subset of (product ()) holds
( P in UniCl () iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

let J be non-Empty TopSpace-yielding ManySortedSet of I; :: thesis: for i being Element of I
for P being Subset of (product ()) holds
( P in UniCl () iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

let i be Element of I; :: thesis: for P being Subset of (product ()) holds
( P in UniCl () iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

card I = 1 by CARD_1:def 7;
then A1: I = {i} by ORDERS_5:2;
the carrier of (J . i) = [#] (J . i) by STRUCT_0:def 3
.= () . i by PENCIL_3:7 ;
then A2: Carrier J = {i} --> the carrier of (J . i) by ;
let P be Subset of (product ()); :: thesis: ( P in UniCl () iff ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

hereby :: thesis: ( ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) implies P in UniCl () )
assume P in UniCl () ; :: thesis: ex V being Element of bool the carrier of (J . i) st
( V is open & P = product ({i} --> V) )

then consider Y being Subset-Family of (product ()) such that
A3: ( Y c= FinMeetCl () & P = union Y ) by CANTOR_1:def 1;
defpred S1[ object ] means ex W being open Subset of (J . i) st
( W = \$1 & product ({i} --> W) in Y );
consider Z being Subset of (bool the carrier of (J . i)) such that
A4: for x being set holds
( x in Z iff ( x in bool the carrier of (J . i) & S1[x] ) ) from reconsider Z = Z as Subset-Family of (J . i) ;
set V = union Z;
take V = union Z; :: thesis: ( V is open & P = product ({i} --> V) )
A5: for W being Subset of (J . i) holds
( W in Z iff ( W is open & product ({i} --> W) in Y ) )
proof
let W be Subset of (J . i); :: thesis: ( W in Z iff ( W is open & product ({i} --> W) in Y ) )
hereby :: thesis: ( W is open & product ({i} --> W) in Y implies W in Z )
assume W in Z ; :: thesis: ( W is open & product ({i} --> W) in Y )
then ex W2 being open Subset of (J . i) st
( W2 = W & product ({i} --> W2) in Y ) by A4;
hence ( W is open & product ({i} --> W) in Y ) ; :: thesis: verum
end;
assume ( W is open & product ({i} --> W) in Y ) ; :: thesis: W in Z
hence W in Z by A4; :: thesis: verum
end;
then for W being Subset of (J . i) st W in Z holds
W is open ;
hence V is open by ; :: thesis: P = product ({i} --> V)
for x being object holds
( x in union Y iff x in product ({i} --> V) )
proof
let x be object ; :: thesis: ( x in union Y iff x in product ({i} --> V) )
hereby :: thesis: ( x in product ({i} --> V) implies x in union Y )
assume x in union Y ; :: thesis: x in product ({i} --> V)
then consider K being set such that
A7: ( x in K & K in Y ) by TARSKI:def 4;
reconsider K = K as Subset of (product ()) by A7;
consider L being Subset of (J . i) such that
A8: ( L is open & K = product ({i} --> L) ) by A3, A7, Lm5;
A9: L in Z by A5, A7, A8;
A10: not L is empty
proof
assume L is empty ; :: thesis: contradiction
then ( dom ({i} --> L) = {i} & rng ({i} --> L) = ) by FUNCOP_1:8;
hence contradiction by A7, A8, Lm1; :: thesis: verum
end;
then consider y being Element of L such that
A11: x = {i} --> y by A7, A8, Th16;
y in V by ;
hence x in product ({i} --> V) by ; :: thesis: verum
end;
assume A12: x in product ({i} --> V) ; :: thesis: x in union Y
A13: not V is empty then consider y being Element of V such that
A14: x = {i} --> y by ;
consider L being set such that
A15: ( y in L & L in Z ) by ;
reconsider L = L as Subset of (J . i) by A15;
reconsider K = product ({i} --> L) as Subset of (product ()) by ;
A16: K in Y by ;
x in K by ;
hence x in union Y by ; :: thesis: verum
end;
hence P = product ({i} --> V) by ; :: thesis: verum
end;
assume ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) ; :: thesis: P in UniCl ()
then P in FinMeetCl () by Lm5;
hence P in UniCl () by ; :: thesis: verum