:: deftheorem Def5 defines canonical_embedding PENCIL_3:def 5 :
for I being non empty finite set
for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is strongly_connected ) holds
for f being Collineation of (Segre_Product A)
for i being Element of I
for b₅ being Function of (A . i),(A . ((permutation_of_indices f) . i)) holds
( b₅ = canonical_embedding (f,i) iff for b being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b is Segre-Coset of A & indx b = i holds
b₅ = canonical_embedding (f,b) );