for I being non empty set
for A being PLS-yielding ManySortedSet of I
for L being non trivial-yielding Segre-like ManySortedSubset of Carrier A
for B being Block of (A . (indx L)) holds product (L +* ((indx L),B)) is Block of (Segre_Product A)