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:

A2: now :: thesis:

let i be Element of I; :: thesis:
A . i is strongly_connected by A1;
hence A . i is connected by Th4; :: thesis:

end;

let f be Collineation of (Segre_Product A); :: thesis:
let B1, B2 be Segre-Coset of A; :: thesis:
let b1, b2, b3, b4 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume that
A3: B1 = product b1 and
A4: B2 = product b2 and
A5: ( f .: B1 = product b3 & f .: B2 = product b4 ) ; :: thesis:
assume A6: indx b1 = indx b2 ; :: thesis:

per cases ;

suppose A7: B1 misses B2 ; :: thesis:

reconsider fB1 = f .: B1, fB2 = f .: B2 as Segre-Coset of A by A1, PENCIL_2:24;
f is bijective Function of the carrier of (Segre_Product A), the carrier of (Segre_Product A) by PENCIL_2:def 4;
then A8: fB1 misses fB2 by A7, FUNCT_1:66;
consider D being FinSequence of bool the carrier of (Segre_Product A) such that
A9: D . 1 = B1 and
A10: D . (len D) = B2 and
A11: for i being Nat st i in dom D holds
D . i is Segre-Coset of A and
A12: for i being Nat st 1 <= i & i < len D holds
for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds
( Di misses Di1 & Di '||' Di1 ) by A2, A3, A4, A6, A7, Th23;
deffunc H₁( Nat) -> Element of bool the carrier of (Segre_Product A) = f .: (D . $1);
consider E being FinSequence of bool the carrier of (Segre_Product A) such that
A13: ( len E = len D & ( for j being Nat st j in dom E holds
E . j = H₁(j) ) ) from FINSEQ_2:sch 1();
A14: dom E = Seg (len D) by A13, FINSEQ_1:def 3;
A15: for i being Nat st 1 <= i & i < len E holds
for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 )

proof

let i be Nat; :: thesis:
A16: f is bijective Function of the carrier of (Segre_Product A), the carrier of (Segre_Product A) by PENCIL_2:def 4;
assume A17: ( 1 <= i & i < len E ) ; :: thesis:
then i in dom D by A13, FINSEQ_3:25;
then reconsider Di = D . i as Segre-Coset of A by A11;
( 1 <= i + 1 & i + 1 <= len E ) by A17, NAT_1:13;
then i + 1 in dom D by A13, FINSEQ_3:25;
then reconsider Di1 = D . (i + 1) as Segre-Coset of A by A11;
let Ei, Ei1 be Segre-Coset of A; :: thesis:
assume that
A18: Ei = E . i and
A19: Ei1 = E . (i + 1) ; :: thesis:
i in Seg (len D) by A13, A17, FINSEQ_1:1;
then A20: Ei = f .: (D . i) by A13, A14, A18;
( 1 <= i + 1 & i + 1 <= len E ) by A17, NAT_1:13;
then i + 1 in Seg (len D) by A13, FINSEQ_1:1;
then A21: Ei1 = f .: (D . (i + 1)) by A13, A14, A19;
Di misses Di1 by A12, A13, A17;
hence Ei misses Ei1 by A20, A21, A16, FUNCT_1:66; :: thesis:
Di '||' Di1 by A12, A13, A17;
hence Ei '||' Ei1 by A20, A21, Th20; :: thesis:

end;

A22: for i being Nat st i in dom E holds
E . i is Segre-Coset of A

proof

let i be Nat; :: thesis:
assume A23: i in dom E ; :: thesis:
then i in Seg (len D) by A13, FINSEQ_1:def 3;
then i in dom D by FINSEQ_1:def 3;
then reconsider di = D . i as Segre-Coset of A by A11;
E . i = f .: di by A13, A23;
hence E . i is Segre-Coset of A by A1, PENCIL_2:24; :: thesis:

end;

len E in dom D by A4, A10, A13, FUNCT_1:def 2;
then len E in Seg (len D) by FINSEQ_1:def 3;
then A24: E . (len E) = f .: B2 by A10, A13, A14;
1 in dom D by A3, A9, FUNCT_1:def 2;
then 1 in Seg (len D) by FINSEQ_1:def 3;
then E . 1 = f .: B1 by A9, A13, A14;
hence indx b3 = indx b4 by A2, A5, A24, A22, A15, A8, Th23; :: thesis:

end;

suppose B1 meets B2 ; :: thesis:

then B1 = B2 by A3, A4, A6, Th11;
hence indx b3 = indx b4 by A5, PUA2MSS1:2; :: thesis:

end;

end;