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