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:
A2: dom f = the carrier of (Segre_Product A) by FUNCT_2:def 1;
let B1, B2 be Segre-Coset of A; :: thesis:
assume A3: ( B1 misses B2 & B1 '||' B2 ) ; :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A4: ( product b1 = B1 & product b2 = B2 ) ; :: thesis:
A5: dom b1 = I by PARTFUN1:def 4;
A6: indx b1 = indx b2 by A3, A4, Th21;
set i = indx b1;
consider r being Element of I such that
A7: ( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) by A3, A4, Th21;
reconsider B3 = f .: B1, B4 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;
f is bijective by PENCIL_2:def 4;
then A8: f is one-to-one ;
then A9: ( B3 misses B4 & B3 '||' B4 ) by A3, Th20, FUNCT_1:125;
consider b3 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A10: ( product b3 = B3 & b3 . (indx b3) = [#] (A . (indx b3)) ) by PENCIL_2:def 2;
consider b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A11: ( product b4 = B4 & b4 . (indx b4) = [#] (A . (indx b4)) ) by PENCIL_2:def 2;
A12: indx b3 = indx b4 by A9, A10, A11, Th21;
set j = indx b3;
A13: ( dom (canonical_embedding f,b1) = the carrier of (A . (indx b1)) & dom (canonical_embedding f,b2) = the carrier of (A . (indx b1)) ) by A6, FUNCT_2:def 1;

now

let o be set ; :: thesis:
assume o in the carrier of (A . (indx b1)) ; :: thesis:
then reconsider u = o as Point of (A . (indx b1)) ;
consider p0 being set such that
A14: p0 in product b1 by XBOOLE_0:def 1;
reconsider p1 = p0 as Point of (Segre_Product A) by A4, A14;
reconsider p = p1 as ManySortedSet of by PENCIL_1:14;
set q = p +* (indx b1),u;
reconsider q1 = p +* (indx b1),u as Point of (Segre_Product A) by PENCIL_1:25;
b1 . r is trivial by A7, PENCIL_1:def 21;
then consider c1 being set such that
A15: b1 . r = {c1} by REALSET1:def 4;
b1 c= Carrier A by PBOOLE:def 23;
then b1 . r c= (Carrier A) . r by PBOOLE:def 5;
then {c1} c= [#] (A . r) by A15, Th7;
then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:37;
b2 . r is trivial by A6, A7, PENCIL_1:def 21;
then consider c2 being set such that
A16: b2 . r = {c2} by REALSET1:def 4;
b2 c= Carrier A by PBOOLE:def 23;
then b2 . r c= (Carrier A) . r by PBOOLE:def 5;
then {c2} c= [#] (A . r) by A16, Th7;
then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:37;
set t = (p +* (indx b1),u) +* r,c2;
p +* (indx b1),u is Point of (Segre_Product A) by PENCIL_1:25;
then reconsider t1 = (p +* (indx b1),u) +* r,c2 as Point of (Segre_Product A) by PENCIL_1:25;

per cases ;

suppose A17: c1 <> c2 ; :: thesis:

(p +* (indx b1),u) . r = p . r by A7, FUNCT_7:34;
then (p +* (indx b1),u) . r in b1 . r by A5, A14, CARD_3:18;
then A18: (p +* (indx b1),u) . r = c1 by A15, TARSKI:def 1;
dom (p +* (indx b1),u) = I by PARTFUN1:def 4;
then A19: ((p +* (indx b1),u) +* r,c2) . r = c2 by FUNCT_7:33;
then A20: f . q1 <> f . t1 by A2, A8, A17, A18, FUNCT_1:def 8;

now

let q3, t3 be ManySortedSet of ; :: thesis:
assume A21: ( q3 = q1 & t3 = t1 ) ; :: thesis:
take r = r; :: thesis:
thus for a, b being Point of (A . r) st a = q3 . r & b = t3 . r holds
( a <> b & a,b are_collinear ) by A7, A15, A16, A17, A18, A19, A21; :: thesis:
let j be Element of I; :: thesis:
assume j <> r ; :: thesis:
hence q3 . j = t3 . j by A21, FUNCT_7:34; :: thesis:

end;

then q1,t1 are_collinear by A17, A18, A19, Th17;
then A22: f . q1,f . t1 are_collinear by Th1;
reconsider fq = f . q1, ft = f . t1 as ManySortedSet of by PENCIL_1:14;
A23: indx b3 = (permutation_of_indices f) . (indx b1) by A1, A4, A10, Def3;
A24: ( dom (p +* (indx b1),u) = I & dom p = I & dom ((p +* (indx b1),u) +* r,c2) = I & dom b1 = I & dom b2 = I ) by PARTFUN1:def 4;

A25: now

let a be set ; :: thesis:
assume A26: a in I ; :: thesis:

per cases ;

suppose a = indx b1 ; :: thesis:

then ( (p +* (indx b1),u) . a = u & b1 . a = [#] (A . (indx b1)) ) by A4, A24, Th10, FUNCT_7:33;
hence (p +* (indx b1),u) . a in b1 . a ; :: thesis:

end;

suppose a <> indx b1 ; :: thesis:

then (p +* (indx b1),u) . a = p . a by FUNCT_7:34;
hence (p +* (indx b1),u) . a in b1 . a by A14, A24, A26, CARD_3:18; :: thesis:

end;

then A27: p +* (indx b1),u in product b1 by A24, CARD_3:18;

now

let a be set ; :: thesis:
assume A28: a in I ; :: thesis:

per cases ;

suppose A29: a = r ; :: thesis:

then ((p +* (indx b1),u) +* r,c2) . a = c2 by A24, FUNCT_7:33;
hence ((p +* (indx b1),u) +* r,c2) . a in b2 . a by A16, A29, TARSKI:def 1; :: thesis:

end;

suppose A30: a <> r ; :: thesis:

then ((p +* (indx b1),u) +* r,c2) . a = (p +* (indx b1),u) . a by FUNCT_7:34;
then ((p +* (indx b1),u) +* r,c2) . a in b1 . a by A25, A28;
hence ((p +* (indx b1),u) +* r,c2) . a in b2 . a by A7, A28, A30; :: thesis:

end;

then A31: (p +* (indx b1),u) +* r,c2 in product b2 by A24, CARD_3:18;
then A32: (canonical_embedding f,b2) . (((p +* (indx b1),u) +* r,c2) . (indx b1)) = ft . ((permutation_of_indices f) . (indx b1)) by A1, A4, A6, Def4;

A33: now

assume A34: fq . (indx b3) <> ft . (indx b3) ; :: thesis:
consider l being Element of I such that
A35: ( ( for a, b being Point of (A . l) st a = fq . l & b = ft . l holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> l holds
fq . j = ft . j ) ) by A20, A22, Th17;
A36: indx b3 = l by A34, A35;
A37: fq in B3 by A2, A4, A27, FUNCT_1:def 12;
A38: ( dom fq = I & dom ft = I & dom b3 = I & dom b4 = I ) by PARTFUN1:def 4;

now

let o be set ; :: thesis:
assume o in I ; :: thesis:
then reconsider o1 = o as Element of I ;

per cases ;

suppose o1 = indx b3 ; :: thesis:

hence fq . o in b4 . o by A10, A11, A12, A37, A38, CARD_3:18; :: thesis:

end;

suppose o1 <> indx b3 ; :: thesis:

then A39: fq . o1 = ft . o1 by A35, A36;
ft in product b4 by A2, A4, A11, A31, FUNCT_1:def 12;
hence fq . o in b4 . o by A38, A39, CARD_3:18; :: thesis:

end;

then fq in product b4 by A38, CARD_3:18;
then fq in (product b3) /\ (product b4) by A10, A37, XBOOLE_0:def 4;
hence contradiction by A9, A10, A11, XBOOLE_0:def 7; :: thesis:

end;

dom p = I by PARTFUN1:def 4;
then A40: (p +* (indx b1),u) . (indx b1) = o by FUNCT_7:33;
then ((p +* (indx b1),u) +* r,c2) . (indx b1) = o by A7, FUNCT_7:34;
hence (canonical_embedding f,b1) . o = (canonical_embedding f,b2) . o by A1, A4, A23, A27, A32, A33, A40, Def4; :: thesis:

end;

suppose A41: c1 = c2 ; :: thesis:

A42: ( dom b1 = I & dom b2 = I ) by PARTFUN1:def 4;

now

let o be set ; :: thesis:
assume o in I ; :: thesis:
then reconsider o1 = o as Element of I ;

per cases ;

suppose r = o1 ; :: thesis:

hence b1 . o = b2 . o by A15, A16, A41; :: thesis:

end;

suppose r <> o1 ; :: thesis:

hence b1 . o = b2 . o by A7; :: thesis:

end;

hence (canonical_embedding f,b1) . o = (canonical_embedding f,b2) . o by A42, FUNCT_1:9; :: thesis:

end;

hence canonical_embedding f,b1 = canonical_embedding f,b2 by A13, FUNCT_1:9; :: thesis: