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 (Segre_Product A)

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 (Segre_Product A)

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 (Segre_Product A)

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

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

for f being Collineation of (Segre_Product A)

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 (Segre_Product A)

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 (Segre_Product A)

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 f be Collineation of (Segre_Product A); :: thesis: for B1, B2 being Segre-Coset of Alet 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;A . i is strongly_connected by A1;

hence A . i is connected by Th4; :: thesis: verum

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 )
;

end;

suppose A7:
B1 misses B2
; :: thesis: indx b3 = indx b4

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_{1}( 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_{1}(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 )

E . i is Segre-Coset of A

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: verum

end;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

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

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

A22:
for i being Nat st i in dom E holds
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 (Segre_Product A), the carrier of (Segre_Product A) 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 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: ( 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 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: Ei '||' Ei1

Di '||' Di1 by A12, A13, A17;

hence Ei '||' Ei1 by A20, A21, Th20; :: thesis: verum

end;( Ei misses Ei1 & Ei '||' Ei1 ) )

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: 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 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: ( 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 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: Ei '||' Ei1

Di '||' Di1 by A12, A13, A17;

hence Ei '||' Ei1 by A20, A21, Th20; :: thesis: verum

E . i is Segre-Coset of A

proof

len E in dom D
by A4, A10, A13, FUNCT_1:def 2;
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 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: verum

end;assume A23: i in dom E ; :: thesis: E . i is Segre-Coset of A

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: verum

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: verum