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 ()) st P in FinMeetCl () holds
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 ()) st P in FinMeetCl () holds
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 ()) st P in FinMeetCl () holds
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 FinMeetCl () implies ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )

assume P in FinMeetCl () ; :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )

then consider X being Subset-Family of (product ()), f being I -valued one-to-one Function such that
A3: ( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X ) and
A4: P = product (() +* ()) by Lm3;
set F = () +* ();
per cases ( rng f = {} or rng f = {i} ) by ;
suppose rng f = {} ; :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )

then a5: product_basis_selector (J,f) = {} ;
take [#] (J . i) ; :: thesis: ( [#] (J . i) is open & P = product ({i} --> ([#] (J . i))) )
thus ( [#] (J . i) is open & P = product ({i} --> ([#] (J . i))) ) by ; :: thesis: verum
end;
suppose A6: rng f = {i} ; :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )

then A7: dom f = {((f ") . i)} by Th1;
A8: i in rng f by ;
A9: (f ") . i in X by ;
then reconsider V0 = (f ") . i as Subset of (product ()) ;
reconsider V = (proj (J,i)) .: V0 as Subset of (J . i) ;
take V ; :: thesis: ( V is open & P = product ({i} --> V) )
( V0 is empty or not V0 is empty ) ;
hence V is open by A3, A9, Th58; :: thesis: P = product ({i} --> V)
A10: product_basis_selector (J,f) = {i} --> (() . i) by
.= {i} --> ((proj (J,i)) .: V0) by ;
dom () = {i} by ;
then dom () = dom () by ;
hence P = product ({i} --> V) by ; :: thesis: verum
end;
end;