let I be non empty finite set ; :: thesis: for A being PLS-yielding ManySortedSet of 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 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 st a = p holds
for b being ManySortedSet of 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 ; :: 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 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 st a = p holds
for b being ManySortedSet of 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 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 st a = p holds
for b being ManySortedSet of 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 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 st a = p holds
for b being ManySortedSet of 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 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 st a = p holds
for b being ManySortedSet of 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₁[ set , set ] means for i being Element of I st i = $1 holds
$2 = canonical_embedding f,i;
A2: for i being set st i in I holds
ex j being set st S₁[i,j]

proof

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

end;

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

now

let x be set ; :: 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 by PARTFUN1:def 4;
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 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 st a = p holds
for b being ManySortedSet of 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 st a = p holds
for b being ManySortedSet of 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 st a = p holds
for b being ManySortedSet of 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 st a = p holds
for b being ManySortedSet of 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 ; :: thesis: ( a = p implies for b being ManySortedSet of 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 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 b be ManySortedSet of ; :: 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 A8: 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 A9: m = B . i ; :: thesis: b . ((permutation_of_indices f) . i) = m . (a . i)
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A10: ( indx b1 = i & product b1 is Segre-Coset of A & a in product b1 ) by A7, Th9;
m = canonical_embedding f,b1 by A1, A4, A9, A10, Def5;
hence b . ((permutation_of_indices f) . i) = m . (a . i) by A1, A7, A8, A10, Def4; :: thesis: verum