for I being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of I
for f being b₁ -valued one-to-one Function
for X being Subset-Family of (product (Carrier J)) st X c= product_prebasis J & dom f = X & f " is non-empty & ( for A being Subset of (product (Carrier J)) st A in X holds
(proj (J,(f /. A))) .: A is open ) holds
for i being Element of I holds
( ( not i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) = [#] (J . i) ) & ( i in rng f implies (proj (J,i)) .: (product ((Carrier J) +* (product_basis_selector (J,f)))) is open ) )