let I be non empty finite set ; :: thesis:
let A be PLS-yielding ManySortedSet of I; :: 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, y, x9 being Element of I st S₁[x,y] & S₁[x9,y] holds
x = x9

proof

reconsider ff = f " as Collineation of (Segre_Product A) by PENCIL_2:13;
let x, y, x9 be Element of I; :: thesis:
assume that
A3: 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 and
A4: 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 = x9 holds
indx b2 = y ; :: thesis:
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A5: indx b1 = x and
A6: product b1 is Segre-Coset of A by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A6;
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
A7: fB1 = product L1 and
L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;
consider b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A8: indx b2 = x9 and
A9: product b2 is Segre-Coset of A by Th8;
reconsider B2 = product b2 as Segre-Coset of A by A9;
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
A10: fB2 = product L2 and
L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;
A11: indx L2 = y by A4, A8, A10;
A12: f is bijective by PENCIL_2:def 4;
A13: ff = f " by A12, TOPS_2:def 4;
then A14: ff .: fB2 = f " fB2 by A12, FUNCT_1:85;
A15: ff .: fB1 = f " fB1 by A12, A13, FUNCT_1:85;
dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
then A16: B2 c= ff .: fB2 by A14, FUNCT_1:76;
ff .: fB2 c= B2 by A12, A14, FUNCT_1:82;
then A17: B2 = ff .: fB2 by A16;
dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
then A18: B1 c= ff .: fB1 by A15, FUNCT_1:76;
ff .: fB1 c= B1 by A12, A15, FUNCT_1:82;
then A19: B1 = ff .: fB1 by A18;
indx L1 = y by A3, A5, A7;
hence x = x9 by A1, A5, A7, A8, A10, A11, A19, A17, Th24; :: thesis:

end;

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

proof

set p0 = the Point of (Segre_Product A);
reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;
let x be Element of I; :: thesis:
reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
dom A = I by PARTFUN1:def 2;
then A . x in rng A by FUNCT_1:3;
then not A . x is trivial by PENCIL_1:def 18;
then reconsider C = [#] (A . x) as non trivial set ;
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 2;
then A21: b . x = C by FUNCT_7:31;
then A22: indx b = x by PENCIL_1:def 21;
product b c= the carrier of (Segre_Product A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in product b ; :: thesis:
then consider f being Function such that
A23: a = f and
A24: dom f = dom b and
A25: for x being object st x in dom b holds
f . x in b . x by CARD_3:def 5;
dom (Carrier A) = I by PARTFUN1:def 2;
then A26: dom f = dom (Carrier A) by A24, PARTFUN1:def 2;

A27: now :: thesis:

let i be object ; :: thesis:
assume A28: i in dom (Carrier A) ; :: thesis:
then reconsider i1 = i as Element of I ;
A29: f . i in b . i by A24, A25, A26, A28;

per cases ;

suppose i1 = x ; :: thesis:

hence f . i in (Carrier A) . i by A21, A29, Th7; :: thesis:

end;

suppose i1 <> x ; :: thesis:

then f . i1 in p . i1 by A29, FUNCT_7:32;
then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;
then f . i1 = p0 . i1 by TARSKI:def 1;
then A30: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;
not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A30; :: 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 A23, A26, A27, CARD_3:def 5; :: thesis:

end;

then reconsider B = product b as Segre-Coset of A by A21, A22, 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
A31: fB = product b0 and
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:
f is bijective by PENCIL_2:def 4;
then rng f = the carrier of (Segre_Product A) by FUNCT_2:def 3;
then A32: f .: fB = product b by FUNCT_1:77;
assume ( B1 = product b1 & f .: B1 = product b2 & indx b1 = y ) ; :: thesis:
hence indx b2 = x by A1, A22, A31, A32, Th24; :: thesis:

end;

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

proof

set p0 = the Point of (Segre_Product A);
reconsider p0 = the Point of (Segre_Product A) as Element of Carrier A by Th6;
let x be Element of I; :: thesis:
reconsider p = {p0} as ManySortedSubset of Carrier A by PENCIL_1:11;
dom A = I by PARTFUN1:def 2;
then A . x in rng A by FUNCT_1:3;
then not A . x is trivial by PENCIL_1:def 18;
then reconsider C = [#] (A . x) as non trivial set ;
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 2;
then A34: b . x = C by FUNCT_7:31;
then A35: indx b = x by PENCIL_1:def 21;
product b c= the carrier of (Segre_Product A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in product b ; :: thesis:
then consider f being Function such that
A36: a = f and
A37: dom f = dom b and
A38: for x being object st x in dom b holds
f . x in b . x by CARD_3:def 5;
dom (Carrier A) = I by PARTFUN1:def 2;
then A39: dom f = dom (Carrier A) by A37, PARTFUN1:def 2;

A40: now :: thesis:

let i be object ; :: thesis:
assume A41: i in dom (Carrier A) ; :: thesis:
then reconsider i1 = i as Element of I ;
A42: f . i in b . i by A37, A38, A39, A41;

per cases ;

suppose i1 = x ; :: thesis:

hence f . i in (Carrier A) . i by A34, A42, Th7; :: thesis:

end;

suppose i1 <> x ; :: thesis:

then f . i1 in p . i1 by A42, FUNCT_7:32;
then f . i1 in {(p0 . i1)} by PZFMISC1:def 1;
then f . i1 = p0 . i1 by TARSKI:def 1;
then A43: f . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;
not [#] (A . i1) is empty ;
then not (Carrier A) . i1 is empty by Th7;
hence f . i in (Carrier A) . i by A43; :: 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 A36, A39, A40, CARD_3:def 5; :: thesis:

end;

then reconsider B = product b as Segre-Coset of A by A34, A35, 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
A44: fB = product b0 and
b0 . (indx b0) = [#] (A . (indx b0)) by PENCIL_2:def 2;
take 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 = indx b0 by A1, A35, A44, Th24; :: thesis:

end;

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

proof

let x, y, y9 be Element of I; :: thesis:
assume that
A46: 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 and
A47: 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 = y9 ; :: thesis:
consider b1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A48: indx b1 = x and
A49: product b1 is Segre-Coset of A by Th8;
reconsider B1 = product b1 as Segre-Coset of A by A49;
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
A50: fB1 = product L1 and
L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;
indx L1 = y by A46, A48, A50;
hence y = y9 by A47, A48, A50; :: 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(A33, A20, A2, A45); :: thesis: