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)) st P in FinMeetCl (product_prebasis J) 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 (Carrier J)) st P in FinMeetCl (product_prebasis J) 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 (Carrier J)) st P in FinMeetCl (product_prebasis J) 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
.= (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 FinMeetCl (product_prebasis J) implies ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) ) )
assume P in FinMeetCl (product_prebasis J) ; :: thesis: ex V being Subset of (J . i) st
( V is open & P = product ({i} --> V) )
then consider X being Subset-Family of (product (Carrier J)), 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 ((Carrier J) +* (product_basis_selector (J,f))) by Lm3;
set F = (Carrier J) +* (product_basis_selector (J,f));
per cases ( rng f = {} or rng f = {i} ) by A1, ZFMISC_1:33;
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 a5, A2, A4, STRUCT_0:def 3; :: 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 A6, TARSKI:def 1;
A9: (f ") . i in X by A3, A7, TARSKI:def 1;
then reconsider V0 = (f ") . i as Subset of (product (Carrier J)) ;
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} --> ((product_basis_selector (J,f)) . i) by A6, Th7
.= {i} --> ((proj (J,i)) .: V0) by A8, Th54 ;
dom (Carrier J) = {i} by A1, PARTFUN1:def 2;
then dom (Carrier J) = dom (product_basis_selector (J,f)) by A6, PARTFUN1:def 2;
hence P = product ({i} --> V) by A4, A10, FUNCT_4:19; :: thesis: verum
end;
end;