:: deftheorem Def4 defines canonical_embedding PENCIL_3:def 4 :
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 b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b1 is Segre-Coset of A holds
for b₅ being Function of (A . (indx b1)),(A . ((permutation_of_indices f) . (indx b1))) holds
( b₅ = canonical_embedding (f,b1) iff ( b₅ is isomorphic & ( for a being ManySortedSet of I st a is Point of (Segre_Product A) & a in product b1 holds
for b being ManySortedSet of I st b = f . a holds
b . ((permutation_of_indices f) . (indx b1)) = b₅ . (a . (indx b1)) ) ) );