theorem Th54: :: TOPS_5:54

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 i being Element of I st i in rng f holds
(product_basis_selector (J,f)) . i = (proj (J,i)) .: ((f ") . i)