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 ()
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4

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 ()
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4 )

assume A1: for i being Element of I holds A . i is strongly_connected ; :: thesis: for f being Collineation of ()
for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4

A2: now :: thesis: for i being Element of I holds A . i is connected
let i be Element of I; :: thesis: A . i is connected
A . i is strongly_connected by A1;
hence A . i is connected by Th4; :: thesis: verum
end;
let f be Collineation of (); :: thesis: for B1, B2 being Segre-Coset of A
for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4

let B1, B2 be Segre-Coset of A; :: thesis: for b1, b2, b3, b4 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 holds
indx b3 = indx b4

let b1, b2, b3, b4 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & B2 = product b2 & f .: B1 = product b3 & f .: B2 = product b4 & indx b1 = indx b2 implies indx b3 = indx b4 )
assume that
A3: B1 = product b1 and
A4: B2 = product b2 and
A5: ( f .: B1 = product b3 & f .: B2 = product b4 ) ; :: thesis: ( not indx b1 = indx b2 or indx b3 = indx b4 )
assume A6: indx b1 = indx b2 ; :: thesis: indx b3 = indx b4
per cases ( B1 misses B2 or B1 meets B2 ) ;
suppose A7: B1 misses B2 ; :: thesis: indx b3 = indx b4
reconsider fB1 = f .: B1, fB2 = f .: B2 as Segre-Coset of A by ;
f is bijective Function of the carrier of (), the carrier of () by PENCIL_2:def 4;
then A8: fB1 misses fB2 by ;
consider D being FinSequence of bool the carrier of () 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 H1( Nat) -> Element of bool the carrier of () = f .: (D . \$1);
consider E being FinSequence of bool the carrier of () such that
A13: ( len E = len D & ( for j being Nat st j in dom E holds
E . j = H1(j) ) ) from A14: dom E = Seg (len D) by ;
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: ( 1 <= i & i < len E implies for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 ) )

A16: f is bijective Function of the carrier of (), the carrier of () by PENCIL_2:def 4;
assume A17: ( 1 <= i & i < len E ) ; :: thesis: for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds
( Ei misses Ei1 & Ei '||' Ei1 )

then i in dom D by ;
then reconsider Di = D . i as Segre-Coset of A by A11;
( 1 <= i + 1 & i + 1 <= len E ) by ;
then i + 1 in dom D by ;
then reconsider Di1 = D . (i + 1) as Segre-Coset of A by A11;
let Ei, Ei1 be Segre-Coset of A; :: thesis: ( Ei = E . i & Ei1 = E . (i + 1) implies ( Ei misses Ei1 & Ei '||' Ei1 ) )
assume that
A18: Ei = E . i and
A19: Ei1 = E . (i + 1) ; :: thesis: ( Ei misses Ei1 & Ei '||' Ei1 )
i in Seg (len D) by ;
then A20: Ei = f .: (D . i) by ;
( 1 <= i + 1 & i + 1 <= len E ) by ;
then i + 1 in Seg (len D) by ;
then A21: Ei1 = f .: (D . (i + 1)) by ;
Di misses Di1 by ;
hence Ei misses Ei1 by ; :: thesis: Ei '||' Ei1
Di '||' Di1 by ;
hence Ei '||' Ei1 by ; :: thesis: verum
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: ( i in dom E implies E . i is Segre-Coset of A )
assume A23: i in dom E ; :: thesis: E . i is Segre-Coset of A
then i in Seg (len D) by ;
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 ;
hence E . i is Segre-Coset of A by ; :: thesis: verum
end;
len E in dom D by ;
then len E in Seg (len D) by FINSEQ_1:def 3;
then A24: E . (len E) = f .: B2 by ;
1 in dom D by ;
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: verum
end;
suppose B1 meets B2 ; :: thesis: indx b3 = indx b4
then B1 = B2 by A3, A4, A6, Th11;
hence indx b3 = indx b4 by ; :: thesis: verum
end;
end;