let I be non empty set ; :: thesis: for A being TopStruct-yielding non-Trivial-yielding ManySortedSet of
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))
let A be TopStruct-yielding non-Trivial-yielding ManySortedSet of ; :: thesis: 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))
let b be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b is Segre-Coset of A implies b . (indx b) = [#] (A . (indx b)) )
assume A1: product b is Segre-Coset of A ; :: thesis: b . (indx b) = [#] (A . (indx b))
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A2: ( product b = product L & L . (indx L) = [#] (A . (indx L)) ) by A1, PENCIL_2:def 2;
b = L by A2, PUA2MSS1:2;
hence b . (indx b) = [#] (A . (indx b)) by A2; :: thesis: verum