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

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