let I be non empty finite set ; :: thesis: 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 ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )
let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is strongly_connected ) implies for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) ) )
assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of (Segre_Product A) ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )
let f be Collineation of (Segre_Product A); :: thesis: ex s being Permutation of I ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . (s . i)) & ( for m being Function of (A . i),(A . (s . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . (s . i)) st m = B . i holds
b . (s . i) = m . (a . i) ) )
set s = permutation_of_indices f;
take permutation_of_indices f ; :: thesis: ex B being Function-yielding ManySortedSet of I st
for i being Element of I holds
( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) ) )
defpred S₁[ object , object ] means for i being Element of I st i = $1 holds
$2 = canonical_embedding (f,i);
A2: for i being object st i in I holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume i in I ; :: thesis: ex j being object st S₁[i,j]
then reconsider i1 = i as Element of I ;
S₁[i1, canonical_embedding (f,i1)] ;
hence ex j being object st S₁[i,j] ; :: thesis: verum

end;

consider B being ManySortedSet of I such that
A3: for i being object st i in I holds
S₁[i,B . i] from PBOOLE:sch 3(A2);

now :: thesis: for x being object st x in dom B holds
B . x is Function

let x be object ; :: thesis: ( x in dom B implies B . x is Function )
assume x in dom B ; :: thesis: B . x is Function
then reconsider y = x as Element of I ;
B . y = canonical_embedding (f,y) by A3;
hence B . x is Function ; :: thesis: verum

end;

then reconsider B = B as Function-yielding ManySortedSet of I by FUNCOP_1:def 6;
take B ; :: thesis: for i being Element of I holds
( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) ) )
let i be Element of I; :: thesis: ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic ) & ( for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) ) )
A4: B . i = canonical_embedding (f,i) by A3;
thus ( B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) & ( for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic ) ) :: thesis: for p being Point of (Segre_Product A)
for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)

proof

thus B . i is Function of (A . i),(A . ((permutation_of_indices f) . i)) by A4; :: thesis: for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
m is isomorphic
let m be Function of (A . i),(A . ((permutation_of_indices f) . i)); :: thesis: ( m = B . i implies m is isomorphic )
assume A5: m = B . i ; :: thesis: m is isomorphic
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A6: ( indx L = i & product L is Segre-Coset of A ) by Th8;
B . i = canonical_embedding (f,L) by A1, A4, A6, Def5;
hence m is isomorphic by A1, A5, A6, Def4; :: thesis: verum

end;

let p be Point of (Segre_Product A); :: thesis: for a being ManySortedSet of I st a = p holds
for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
let a be ManySortedSet of I; :: thesis: ( a = p implies for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) )
assume A7: a = p ; :: thesis: for b being ManySortedSet of I st b = f . p holds
for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A8: ( indx b1 = i & product b1 is Segre-Coset of A ) and
A9: a in product b1 by A7, Th9;
let b be ManySortedSet of I; :: thesis: ( b = f . p implies for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i) )
assume A10: b = f . p ; :: thesis: for m being Function of (A . i),(A . ((permutation_of_indices f) . i)) st m = B . i holds
b . ((permutation_of_indices f) . i) = m . (a . i)
let m be Function of (A . i),(A . ((permutation_of_indices f) . i)); :: thesis: ( m = B . i implies b . ((permutation_of_indices f) . i) = m . (a . i) )
assume m = B . i ; :: thesis: b . ((permutation_of_indices f) . i) = m . (a . i)
then m = canonical_embedding (f,b1) by A1, A4, A8, Def5;
hence b . ((permutation_of_indices f) . i) = m . (a . i) by A1, A7, A10, A8, A9, Def4; :: thesis: verum