theorem Th10: :: PENCIL_3:10

for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A holds
b . (indx b) = [#] (A . (indx b))