let I be non empty finite set ; :: thesis:
let A be PLS-yielding ManySortedSet of ; :: thesis:
assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis:
let f be Collineation of (Segre_Product A); :: thesis:
defpred S₁[ set , set ] means 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 = $1 holds
indx b2 = $2;
A2: for x being Element of I ex y being Element of I st S₁[x,y]

proof

let x be Element of I; :: thesis:
dom A = I by PARTFUN1:def 4;
then A . x in rng A by FUNCT_1:12;
then not A . x is trivial by PENCIL_1:def 18;
then reconsider C = [#] (A . x) as non trivial set ;
consider p0 being Point of (Segre_Product A);
reconsider p0 = p0 as Element of Carrier A by Th6;
reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider b = p +* x,C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
dom p = I by PARTFUN1:def 4;
then A3: b . x = C by FUNCT_7:33;
then A4: indx b = x by PENCIL_1:def 21;
product b c= the carrier of (Segre_Product A)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in product b ; :: thesis:
then consider f being Function such that
A5: ( a = f & dom f = dom b & ( for x being set st x in dom b holds
f . x in b . x ) ) by CARD_3:def 5;
dom (Carrier A) = I by PARTFUN1:def 4;
then A6: dom f = dom (Carrier A) by A5, PARTFUN1:def 4;

A7: now

let i be set ; :: thesis:
assume A8: i in dom (Carrier A) ; :: thesis:
then A9: f . i in b . i by A5, A6;
reconsider i1 = i as Element of I by A8, PARTFUN1:def 4;

per cases ;

suppose i1 = x ; :: thesis:

hence f . i in (Carrier A) . i by A3, A9, Th7; :: thesis:

end;

suppose i1 <> x ; :: thesis:

then f . i1 in p . i1 by A9, FUNCT_7:34;
then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;
then f . i1 = p0 . i1 by TARSKI:def 1;
then A10: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 17;
not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A10; :: thesis:

end;

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def 23;
hence a in the carrier of (Segre_Product A) by A5, A6, A7, CARD_3:def 5; :: thesis:

end;

then reconsider B = product b as Segre-Coset of A by A3, A4, PENCIL_2:def 2;
reconsider fB = f .: B as Segre-Coset of A by A1, PENCIL_2:24;
consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A11: ( fB = product b0 & b0 . (indx b0) = [#] (A . (indx b0)) ) by PENCIL_2:def 2;
take y = indx b0; :: thesis:
let B1 be Segre-Coset of A; :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = x ) ; :: thesis:
hence indx b2 = y by A1, A4, A11, Th24; :: thesis:

end;

A12: for y being Element of I ex x being Element of I st S₁[x,y]

proof

let x be Element of I; :: thesis:
dom A = I by PARTFUN1:def 4;
then A . x in rng A by FUNCT_1:12;
then not A . x is trivial by PENCIL_1:def 18;
then reconsider C = [#] (A . x) as non trivial set ;
consider p0 being Point of (Segre_Product A);
reconsider p0 = p0 as Element of Carrier A by Th6;
reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
reconsider b = p +* x,C as non trivial-yielding Segre-like ManySortedSubset of Carrier A by PENCIL_1:9, PENCIL_1:10, PENCIL_2:7;
dom p = I by PARTFUN1:def 4;
then A13: b . x = C by FUNCT_7:33;
then A14: indx b = x by PENCIL_1:def 21;
product b c= the carrier of (Segre_Product A)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in product b ; :: thesis:
then consider f being Function such that
A15: ( a = f & dom f = dom b & ( for x being set st x in dom b holds
f . x in b . x ) ) by CARD_3:def 5;
dom (Carrier A) = I by PARTFUN1:def 4;
then A16: dom f = dom (Carrier A) by A15, PARTFUN1:def 4;

A17: now

let i be set ; :: thesis:
assume A18: i in dom (Carrier A) ; :: thesis:
then A19: f . i in b . i by A15, A16;
reconsider i1 = i as Element of I by A18, PARTFUN1:def 4;

per cases ;

suppose i1 = x ; :: thesis:

hence f . i in (Carrier A) . i by A13, A19, Th7; :: thesis:

end;

suppose i1 <> x ; :: thesis:

then f . i1 in p . i1 by A19, FUNCT_7:34;
then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;
then f . i1 = p0 . i1 by TARSKI:def 1;
then A20: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 17;
not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A20; :: thesis:

end;

Segre_Product A = TopStruct(# (product (Carrier A)),(Segre_Blocks A) #) by PENCIL_1:def 23;
hence a in the carrier of (Segre_Product A) by A15, A16, A17, CARD_3:def 5; :: thesis:

end;

then reconsider B = product b as Segre-Coset of A by A13, A14, PENCIL_2:def 2;
reconsider fB = f " B as Segre-Coset of A by A1, PENCIL_2:25;
consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A21: ( fB = product b0 & b0 . (indx b0) = [#] (A . (indx b0)) ) by PENCIL_2:def 2;
take y = indx b0; :: thesis:
let B1 be Segre-Coset of A; :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A22: ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y ) ; :: thesis:
f is bijective by PENCIL_2:def 4;
then f is onto ;
then rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;
then f .: fB = product b by FUNCT_1:147;
hence indx b2 = x by A1, A14, A21, A22, Th24; :: thesis:

end;

A23: for x, y, x' being Element of I st S₁[x,y] & S₁[x',y] holds
x = x'

proof

let x, y, x' be Element of I; :: thesis:
assume A24: ( ( 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 = x holds
indx b2 = y ) & ( 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 = x' holds
indx b2 = y ) ) ; :: thesis:
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A25: ( indx b1 = x & product b1 is Segre-Coset of A ) by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A25;
reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A26: ( fB1 = product L1 & L1 . (indx L1) = [#] (A . (indx L1)) ) by PENCIL_2:def 2;
A27: indx L1 = y by A24, A25, A26;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A28: ( indx b2 = x' & product b2 is Segre-Coset of A ) by Th8;
reconsider B2 = product b2 as Segre-Coset of A by A28;
reconsider fB2 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;
consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A29: ( fB2 = product L2 & L2 . (indx L2) = [#] (A . (indx L2)) ) by PENCIL_2:def 2;
A30: indx L2 = y by A24, A28, A29;
reconsider ff = f " as Collineation of (Segre_Product A) by PENCIL_2:13;
f is bijective by PENCIL_2:def 4;
then A31: ( f is onto & f is one-to-one ) ;
then rng f = [#] (Segre_Product A) by FUNCT_2:def 3;
then A32: ff = f " by A31, TOPS_2:def 4;
then A33: ff .: fB1 = f " fB1 by A31, FUNCT_1:155;
then A34: ff .: fB1 c= B1 by A31, FUNCT_1:152;
dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
then B1 c= ff .: fB1 by A33, FUNCT_1:146;
then A35: B1 = ff .: fB1 by A34, XBOOLE_0:def 10;
A36: ff .: fB2 = f " fB2 by A31, A32, FUNCT_1:155;
then A37: ff .: fB2 c= B2 by A31, FUNCT_1:152;
dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
then B2 c= ff .: fB2 by A36, FUNCT_1:146;
then B2 = ff .: fB2 by A37, XBOOLE_0:def 10;
hence x = x' by A1, A25, A26, A27, A28, A29, A30, A35, Th24; :: thesis:

end;

A38: for x, y, y' being Element of I st S₁[x,y] & S₁[x,y'] holds
y = y'

proof

let x, y, y' be Element of I; :: thesis:
assume A39: ( ( 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 = x holds
indx b2 = y ) & ( 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 = x holds
indx b2 = y' ) ) ; :: thesis:
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A40: ( indx b1 = x & product b1 is Segre-Coset of A ) by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A40;
reconsider fB1 = f .: B1 as Segre-Coset of A by A1, PENCIL_2:24;
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A41: ( fB1 = product L1 & L1 . (indx L1) = [#] (A . (indx L1)) ) by PENCIL_2:def 2;
indx L1 = y by A39, A40, A41;
hence y = y' by A39, A40, A41; :: thesis:

end;

thus ex f being Permutation of I st
for x, y being Element of I holds
( f . x = y iff S₁[x,y] ) from TRANSGEO:sch 1(A2, A12, A23, A38); :: thesis: