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_{1}[ 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_{1}[i,j]

A3: for i being object st i in I holds

S_{1}[i,B . i]
from PBOOLE:sch 3(A2);

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)

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

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

$2 = canonical_embedding (f,i);

A2: for i being object st i in I holds

ex j being object st S

proof

consider B being ManySortedSet of I such that
let i be object ; :: thesis: ( i in I implies ex j being object st S_{1}[i,j] )

assume i in I ; :: thesis: ex j being object st S_{1}[i,j]

then reconsider i1 = i as Element of I ;

S_{1}[i1, canonical_embedding (f,i1)]
;

hence ex j being object st S_{1}[i,j]
; :: thesis: verum

end;assume i in I ; :: thesis: ex j being object st S

then reconsider i1 = i as Element of I ;

S

hence ex j being object st S

A3: for i being object st i in I holds

S

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

B . x is Function

then reconsider B = B as Function-yielding ManySortedSet of I by FUNCOP_1:def 6;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;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

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

let p be Point of (Segre_Product A); :: thesis: for a being ManySortedSet of I st a = p holds
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;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

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