for I being non empty set
for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I holds <:(proj (J,i)),(proj (J,j)):> is Function of (product J),[:(J . i),(J . j):] by BORSUK_1:def 2;