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 connected ; :: thesis:
let i be Element of I; :: thesis:
let p be Point of (A . i); :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume that
A2: product b2 is Segre-Coset of A and
A3: b1 = b2 +* (i,{p}) and
A4: not p in b2 . i ; :: thesis:
defpred S₁[ set , set ] means for a, b being Point of (A . i) st $1 = a & $2 = b holds
a,b are_collinear ;

A5: now :: thesis:

assume i = indx b2 ; :: thesis:
then b2 . i = [#] (A . i) by A2, Th10;
hence contradiction by A4; :: thesis:

end;

then b2 . i is 1 -element by PENCIL_1:12;
then consider q being object such that
A6: b2 . i = {q} by ZFMISC_1:131;
b2 c= Carrier A by PBOOLE:def 18;
then b2 . i c= (Carrier A) . i ;
then {q} c= [#] (A . i) by A6, Th7;
then reconsider q = q as Point of (A . i) by ZFMISC_1:31;
A . i is connected by A1;
then consider f being FinSequence of the carrier of (A . i) such that
A7: ( p = f . 1 & q = f . (len f) ) and
A8: for j being Nat st 1 <= j & j < len f holds
for a, b being Point of (A . i) st a = f . j & b = f . (j + 1) holds
a,b are_collinear by PENCIL_1:def 10;
A9: for j being Element of NAT
for x, y being set st 1 <= j & j < len f & x = f . j & y = f . (j + 1) holds
S₁[x,y] by A8;
consider F being one-to-one FinSequence of the carrier of (A . i) such that
A10: ( p = F . 1 & q = F . (len F) & rng F c= rng f & ( for j being Element of NAT st 1 <= j & j < len F holds
S₁[F . j,F . (j + 1)] ) ) from PENCIL_2:sch 1(A7, A9);

A11: now :: thesis:

assume F = {} ; :: thesis:
then dom F = {} ;
then ( F . 1 = {} & F . (len F) = {} ) by FUNCT_1:def 2;
hence contradiction by A4, A6, A10, TARSKI:def 1; :: thesis:

end;

deffunc H₁( set ) -> set = product (b2 +* (i,{(F . $1)}));
consider G being FinSequence such that
A12: ( len G = len F & ( for j being Nat st j in dom G holds
G . j = H₁(j) ) ) from FINSEQ_1:sch 2();
rng G c= bool the carrier of (Segre_Product A)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng G ; :: thesis:
then consider o being object such that
A13: o in dom G and
A14: G . o = a by FUNCT_1:def 3;
reconsider o = o as Element of NAT by A13;
dom G = dom F by A12, FINSEQ_3:29;
then F . o in rng F by A13, FUNCT_1:3;
then {(F . o)} is Subset of (A . i) by ZFMISC_1:31;
then A15: product (b2 +* (i,{(F . o)})) is Subset of (Segre_Product A) by Th14;
G . o = product (b2 +* (i,{(F . o)})) by A12, A13;
hence a in bool the carrier of (Segre_Product A) by A14, A15; :: thesis:

end;

then reconsider D = G as FinSequence of bool the carrier of (Segre_Product A) by FINSEQ_1:def 4;
take D ; :: thesis:
A16: dom G = Seg (len F) by A12, FINSEQ_1:def 3;
dom F = Seg (len F) by FINSEQ_1:def 3;
hence D . 1 = product b1 by A3, A10, A12, A16, A11, FINSEQ_3:32; :: thesis:
D . (len D) = product (b2 +* (i,{(F . (len F))})) by A12, A16, A11, FINSEQ_1:3;
hence D . (len D) = product b2 by A6, A10, FUNCT_7:35; :: thesis:
thus for j being Nat st j in dom D holds
D . j is Segre-Coset of A :: thesis:

proof

let j be Nat; :: thesis:
assume A17: j in dom D ; :: thesis:
then j in Seg (len F) by A12, FINSEQ_1:def 3;
then j in dom F by FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:3;
then reconsider Fj = F . j as Point of (A . i) ;
reconsider BB = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;
BB . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;
then not BB . (indx b2) is trivial by PENCIL_1:def 21;
then A18: indx BB = indx b2 by PENCIL_1:def 21;
then A19: BB . (indx BB) = b2 . (indx b2) by A5, FUNCT_7:32
.= [#] (A . (indx BB)) by A2, A18, Th10 ;
A20: D . j = product BB by A12, A17;
then D . j is Subset of (Segre_Product A) by Th14;
hence D . j is Segre-Coset of A by A20, A19, PENCIL_2:def 2; :: thesis:

end;

A21: dom b2 = I by PARTFUN1:def 2;
thus 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 ) :: thesis:

proof

let j be Nat; :: thesis:
assume A22: ( 1 <= j & j < len D ) ; :: thesis:
let Di, Di1 be Segre-Coset of A; :: thesis:
assume that
A23: Di = D . j and
A24: Di1 = D . (j + 1) ; :: thesis:
reconsider j = j as Element of NAT by ORDINAL1:def 12;
j in dom D by A22, FINSEQ_3:25;
then j in Seg (len F) by A12, FINSEQ_1:def 3;
then j in dom F by FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:3;
then reconsider Fj = F . j as Point of (A . i) ;
reconsider BB1 = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;
A25: j in dom D by A22, FINSEQ_3:25;
then A26: D . j = product BB1 by A12;
( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13;
then j + 1 in dom D by FINSEQ_3:25;
then j + 1 in Seg (len F) by A12, FINSEQ_1:def 3;
then j + 1 in dom F by FINSEQ_1:def 3;
then F . (j + 1) in rng F by FUNCT_1:3;
then reconsider Fj2 = F . (j + 1) as Point of (A . i) ;
reconsider BB2 = b2 +* (i,{Fj2}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;
( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13;
then A27: j + 1 in dom D by FINSEQ_3:25;
then A28: j + 1 in Seg (len F) by A12, FINSEQ_1:def 3;
A29: D . (j + 1) = product BB2 by A12, A27;
A30: j in Seg (len F) by A12, A25, FINSEQ_1:def 3;
thus A31: Di misses Di1 :: thesis:

proof

A32: j <> j + 1 ;
assume Di /\ Di1 <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider x being object such that
A33: x in Di /\ Di1 by XBOOLE_0:def 1;
x in Di1 by A33, XBOOLE_0:def 4;
then consider x2 being Function such that
A34: x2 = x and
dom x2 = dom (b2 +* (i,{(F . (j + 1))})) and
A35: for o being object st o in dom (b2 +* (i,{(F . (j + 1))})) holds
x2 . o in (b2 +* (i,{(F . (j + 1))})) . o by A24, A29, CARD_3:def 5;
dom (b2 +* (i,{(F . (j + 1))})) = I by PARTFUN1:def 2;
then x2 . i in (b2 +* (i,{(F . (j + 1))})) . i by A35;
then x2 . i in {(F . (j + 1))} by A21, FUNCT_7:31;
then A36: x2 . i = F . (j + 1) by TARSKI:def 1;
x in Di by A33, XBOOLE_0:def 4;
then consider x1 being Function such that
A37: x1 = x and
dom x1 = dom (b2 +* (i,{(F . j)})) and
A38: for o being object st o in dom (b2 +* (i,{(F . j)})) holds
x1 . o in (b2 +* (i,{(F . j)})) . o by A23, A26, CARD_3:def 5;
dom (b2 +* (i,{(F . j)})) = I by PARTFUN1:def 2;
then x1 . i in (b2 +* (i,{(F . j)})) . i by A38;
then x1 . i in {(F . j)} by A21, FUNCT_7:31;
then A39: x1 . i = F . j by TARSKI:def 1;
( j in dom F & j + 1 in dom F ) by A30, A28, FINSEQ_1:def 3;
hence contradiction by A37, A34, A39, A36, A32, FUNCT_1:def 4; :: thesis:

end;

now :: thesis:

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume that
A40: Di = product c1 and
A41: Di1 = product c2 ; :: thesis:
A42: c2 = b2 +* (i,{(F . (j + 1))}) by A24, A29, A41, PUA2MSS1:2;
then c2 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;
then A43: not c2 . (indx b2) is trivial by PENCIL_1:def 21;
A44: c1 = b2 +* (i,{(F . j)}) by A23, A26, A40, PUA2MSS1:2;
then c1 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;
then A45: not c1 . (indx b2) is trivial by PENCIL_1:def 21;
then indx c1 = indx b2 by PENCIL_1:def 21;
hence indx c1 = indx c2 by A43, PENCIL_1:def 21; :: thesis:
take r = i; :: thesis:
thus r <> indx c1 by A5, A45, PENCIL_1:def 21; :: thesis:
thus for j being Element of I st j <> r holds
c1 . j = c2 . j :: thesis:

proof

let j be Element of I; :: thesis:
assume A46: j <> r ; :: thesis:
hence c1 . j = b2 . j by A44, FUNCT_7:32
.= c2 . j by A42, A46, FUNCT_7:32 ;
:: thesis:

end;

thus for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
p1,p2 are_collinear :: thesis:

proof

let p1, p2 be Point of (A . r); :: thesis:
assume that
A47: c1 . r = {p1} and
A48: c2 . r = {p2} ; :: thesis:
c2 . r = {(F . (j + 1))} by A21, A42, FUNCT_7:31;
then A49: F . (j + 1) = p2 by A48, ZFMISC_1:3;
c1 . r = {(F . j)} by A21, A44, FUNCT_7:31;
then F . j = p1 by A47, ZFMISC_1:3;
hence p1,p2 are_collinear by A10, A12, A22, A49; :: thesis:

end;

hence Di '||' Di1 by A31, Th21; :: thesis:

end;