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) ) )

( 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

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
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_{1}[ 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_{1}[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 ) )

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) )

end;( 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

( 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

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

then
for W being Subset of (J . i) st W in Z holds
let W be Subset of (J . i); :: thesis: ( W in Z iff ( W is open & product ({i} --> W) in Y ) )

hence W in Z by A4; :: thesis: verum

end;hereby :: thesis: ( W is open & product ({i} --> W) in Y implies W in Z )

assume
( W is open & product ({i} --> W) in Y )
; :: thesis: W in Zassume
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;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

hence W in Z by A4; :: thesis: verum

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

hence
P = product ({i} --> V)
by A3, TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in union Y iff x in product ({i} --> V) )

A13: not V is empty

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;hereby :: thesis: ( x in product ({i} --> V) implies x in union Y )

assume A12:
x in product ({i} --> V)
; :: thesis: x in union Yassume
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

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;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

then consider y being Element of L such that
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 ( dom ({i} --> L) = {i} & rng ({i} --> L) = {{}} ) by FUNCOP_1:8;

hence contradiction by A7, A8, Lm1; :: thesis: verum

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

A13: not V is empty

proof

then consider y being Element of V such that
assume
V is empty
; :: thesis: contradiction

then rng ({i} --> V) = {{}} by FUNCOP_1:8;

hence contradiction by A12, Lm1; :: thesis: verum

end;then rng ({i} --> V) = {{}} by FUNCOP_1:8;

hence contradiction by A12, Lm1; :: thesis: verum

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

( 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