theorem Th25: :: PENCIL_3:25

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) ex s being Permutation of I st
for i, j being Element of I holds
( s . 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 )