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 (Carrier J)) holds
( P in UniCl (FinMeetCl (product_prebasis J)) 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 (Carrier J)) holds
( P in UniCl (FinMeetCl (product_prebasis J)) 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 (Carrier J)) holds
( P in UniCl (FinMeetCl (product_prebasis J)) 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
.= (Carrier J) . i by PENCIL_3:7 ;
then A2: Carrier J = {i} --> the carrier of (J . i) by A1, Th7;
let P be Subset of (product (Carrier J)); :: thesis: ( P in UniCl (FinMeetCl (product_prebasis J)) 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 (FinMeetCl (product_prebasis J)) )

assume P in UniCl (FinMeetCl (product_prebasis J)) ; :: 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 (Carrier J)) such that
A3: ( Y c= FinMeetCl (product_prebasis J) & P = union Y ) by CANTOR_1:def 1;
defpred S₁[ 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) & S₁[x] ) ) from SUBSET_1:sch 1();
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 TOPS_2:def 1, TOPS_2:19; :: 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 (Carrier J)) 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 A9, A10, TARSKI:def 4;
hence x in product ({i} --> V) by A11, Th16; :: thesis: verum

end;

assume A12: x in product ({i} --> V) ; :: thesis: x in union Y
A13: not V is empty

proof

assume V is empty ; :: thesis: contradiction
then rng ({i} --> V) = {{}} by FUNCOP_1:8;
hence contradiction by A12, Lm1; :: thesis: verum

end;

then consider y being Element of V such that
A14: x = {i} --> y by A12, Th16;
consider L being set such that
A15: ( y in L & L in Z ) by A13, TARSKI:def 4;
reconsider L = L as Subset of (J . i) by A15;
reconsider K = product ({i} --> L) as Subset of (product (Carrier J)) by A2, Th14;
A16: K in Y by A5, A15;
x in K by A14, A15, Th16;
hence x in union Y by A16, TARSKI:def 4; :: thesis: verum

end;

hence P = product ({i} --> V) by A3, TARSKI:2; :: thesis: verum

end;

assume ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) ; :: thesis: P in UniCl (FinMeetCl (product_prebasis J))
then P in FinMeetCl (product_prebasis J) by Lm5;
hence P in UniCl (FinMeetCl (product_prebasis J)) by CANTOR_1:1, TARSKI:def 3; :: thesis: verum