for I being non empty set
for i being Element of I
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for p being Point of (Segre_Product A) ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( indx L = i & product L is Segre-Coset of A & p in product L )