consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A2: indx L = i and
A3: product L is Segre-Coset of A by Th8;
reconsider n = canonical_embedding (f,L) as Function of (A . i),(A . ((permutation_of_indices f) . i)) by A2;
take n ; :: 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
n = canonical_embedding (f,b)
let b be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b is Segre-Coset of A & indx b = i implies n = canonical_embedding (f,b) )
assume ( product b is Segre-Coset of A & indx b = i ) ; :: thesis: n = canonical_embedding (f,b)
hence n = canonical_embedding (f,b) by A1, A2, A3, Th27; :: thesis: verum