theorem Th55: :: TOPS_5:55

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 st f " is non-empty & dom f c= bool (product (Carrier J)) holds
product_basis_selector (J,f) is non-empty