:: deftheorem Def3 defines permutation_of_indices PENCIL_3:def 3 :
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 b₄ being Permutation of I holds
( b₄ = permutation_of_indices f iff for i, j being Element of I holds
( b₄ . i = j iff for B1 being Segre-Coset of A
for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & f .: B1 = product b2 & indx b1 = i holds
indx b2 = j ) );