:: deftheorem defines product_basis_selector TOPS_5:def 4 :
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 holds product_basis_selector (J,f) = ((ProjMap J) .:.: (I -indexing (f "))) | (rng f);