let n1, n2 be Function of (A . i),(A . ((permutation_of_indices f) . i)); :: thesis: ( ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n1 = canonical_embedding (f,b) ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n2 = canonical_embedding (f,b) ) implies n1 = n2 )

assume that

A4: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n1 = canonical_embedding (f,b) and

A5: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n2 = canonical_embedding (f,b) ; :: thesis: n1 = n2

consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A6: ( indx L = i & product L is Segre-Coset of A ) by Th8;

thus n1 = canonical_embedding (f,L) by A4, A6

.= n2 by A5, A6 ; :: thesis: verum

n1 = canonical_embedding (f,b) ) & ( for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n2 = canonical_embedding (f,b) ) implies n1 = n2 )

assume that

A4: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n1 = canonical_embedding (f,b) and

A5: for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds

n2 = canonical_embedding (f,b) ; :: thesis: n1 = n2

consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A6: ( indx L = i & product L is Segre-Coset of A ) by Th8;

thus n1 = canonical_embedding (f,L) by A4, A6

.= n2 by A5, A6 ; :: thesis: verum