for p being RelStr-yielding ManySortedSet of {0}
for z being Element of {0} holds p . z, product p are_isomorphic