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

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