:: deftheorem Def2 defines Segre-Coset PENCIL_2:def 2 :
for I being non empty set
for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of I
for b₃ being Subset of (Segre_Product A) holds
( b₃ is Segre-Coset of A iff ex L being non trivial-yielding Segre-like ManySortedSubset of Carrier A st
( b₃ = product L & L . (indx L) = [#] (A . (indx L)) ) );