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