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 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 A2: ( product b1 is Segre-Coset of A & product b2 is Segre-Coset of A & b1 = b2 +* i,{p} & not p in b2 . i ) ; :: thesis:
A3: dom b2 = I by PARTFUN1:def 4;

A4: now

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

end;

then ( not b2 . i is empty & b2 . i is trivial ) by PENCIL_1:12;
then consider q being set such that
A5: b2 . i = {q} by REALSET1:def 4;
b2 c= Carrier A by PBOOLE:def 23;
then b2 . i c= (Carrier A) . i by PBOOLE:def 5;
then {q} c= [#] (A . i) by A5, Th7;
then reconsider q = q as Point of (A . i) by ZFMISC_1:37;
A . i is connected by A1;
then consider f being FinSequence of the carrier of (A . i) such that
A6: ( p = f . 1 & q = f . (len f) ) and
A7: 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;
defpred S₁[ set , set ] means for a, b being Point of (A . i) st $1 = a & $2 = b holds
a,b are_collinear ;
A8: 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 A7;
consider F being one-to-one FinSequence of the carrier of (A . i) such that
A9: ( 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(A6, A8);
deffunc H₁( set ) -> set = product (b2 +* i,{(F . $1)});
consider G being FinSequence such that
A10: ( len G = len F & ( for j being Nat st j in dom G holds
G . j = H₁(j) ) ) from FINSEQ_1:sch 2();
A11: dom G = Seg (len F) by A10, FINSEQ_1:def 3;
rng G c= bool the carrier of (Segre_Product A)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in rng G ; :: thesis:
then consider o being set such that
A12: ( o in dom G & G . o = a ) by FUNCT_1:def 5;
reconsider o = o as Element of NAT by A12;
o in Seg (len F) by A10, A12, FINSEQ_1:def 3;
then A13: G . o = product (b2 +* i,{(F . o)}) by A10, A11;
dom G = dom F by A10, FINSEQ_3:31;
then F . o in rng F by A12, FUNCT_1:12;
then {(F . o)} is Subset of (A . i) by ZFMISC_1:37;
then product (b2 +* i,{(F . o)}) is Subset of (Segre_Product A) by Th14;
hence a in bool the carrier of (Segre_Product A) by A12, A13; :: thesis:

end;

then reconsider D = G as FinSequence of bool the carrier of (Segre_Product A) by FINSEQ_1:def 4;
take D ; :: thesis:

A14: now

assume F = {} ; :: thesis:
then dom F = {} ;
then ( F . 1 = {} & F . (len F) = {} ) by FUNCT_1:def 4;
hence contradiction by A2, A5, A9, TARSKI:def 1; :: thesis:

end;

then rng F <> {} ;
then A15: 1 in dom F by FINSEQ_3:34;
dom F = Seg (len F) by FINSEQ_1:def 3;
hence D . 1 = product b1 by A2, A9, A10, A15, A11; :: thesis:
len F <> 0 by A14;
then D . (len D) = product (b2 +* i,{(F . (len F))}) by A10, A11, FINSEQ_1:5;
hence D . (len D) = product b2 by A5, A9, FUNCT_7:37; :: 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 A16: j in dom D ; :: thesis:
then j in Seg (len F) by A10, FINSEQ_1:def 3;
then j in dom F by FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:12;
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 A4, Th13;
j in Seg (len F) by A10, A16, FINSEQ_1:def 3;
then A17: D . j = product BB by A10, A11;
then A18: D . j is Subset of (Segre_Product A) by Th14;
BB . (indx b2) = b2 . (indx b2) by A4, FUNCT_7:34;
then not BB . (indx b2) is trivial by PENCIL_1:def 21;
then A19: indx BB = indx b2 by PENCIL_1:def 21;
then BB . (indx BB) = b2 . (indx b2) by A4, FUNCT_7:34
.= [#] (A . (indx BB)) by A2, A19, Th10 ;
hence D . j is Segre-Coset of A by A17, A18, PENCIL_2:def 2; :: thesis:

end;

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 A20: ( 1 <= j & j < len D ) ; :: thesis:
let Di, Di1 be Segre-Coset of A; :: thesis:
assume A21: ( Di = D . j & Di1 = D . (j + 1) ) ; :: thesis:
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j in dom D by A20, FINSEQ_3:27;
then j in Seg (len F) by A10, FINSEQ_1:def 3;
then j in dom F by FINSEQ_1:def 3;
then F . j in rng F by FUNCT_1:12;
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 A4, Th13;
( 1 <= j + 1 & j + 1 <= len D ) by A20, NAT_1:13;
then j + 1 in dom D by FINSEQ_3:27;
then j + 1 in Seg (len F) by A10, 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:12;
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 A4, Th13;
j in dom D by A20, FINSEQ_3:27;
then A22: j in Seg (len F) by A10, FINSEQ_1:def 3;
then A23: D . j = product BB1 by A10, A11;
( 1 <= j + 1 & j + 1 <= len D ) by A20, NAT_1:13;
then j + 1 in dom D by FINSEQ_3:27;
then A24: j + 1 in Seg (len F) by A10, FINSEQ_1:def 3;
then A25: D . (j + 1) = product BB2 by A10, A11;
thus A26: Di misses Di1 :: thesis:

proof

assume Di /\ Di1 <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
then consider x being set such that
A27: x in Di /\ Di1 by XBOOLE_0:def 1;
A28: ( x in Di & x in Di1 ) by A27, XBOOLE_0:def 4;
then consider x1 being Function such that
A29: ( x1 = x & dom x1 = dom (b2 +* i,{(F . j)}) & ( for o being set st o in dom (b2 +* i,{(F . j)}) holds
x1 . o in (b2 +* i,{(F . j)}) . o ) ) by A21, A23, CARD_3:def 5;
consider x2 being Function such that
A30: ( x2 = x & dom x2 = dom (b2 +* i,{(F . (j + 1))}) & ( for o being set st o in dom (b2 +* i,{(F . (j + 1))}) holds
x2 . o in (b2 +* i,{(F . (j + 1))}) . o ) ) by A21, A25, A28, CARD_3:def 5;
dom (b2 +* i,{(F . j)}) = I by PARTFUN1:def 4;
then x1 . i in (b2 +* i,{(F . j)}) . i by A29;
then x1 . i in {(F . j)} by A3, FUNCT_7:33;
then A31: x1 . i = F . j by TARSKI:def 1;
dom (b2 +* i,{(F . (j + 1))}) = I by PARTFUN1:def 4;
then x2 . i in (b2 +* i,{(F . (j + 1))}) . i by A30;
then x2 . i in {(F . (j + 1))} by A3, FUNCT_7:33;
then A32: x2 . i = F . (j + 1) by TARSKI:def 1;
( j in dom F & j + 1 in dom F & j <> j + 1 ) by A22, A24, FINSEQ_1:def 3;
hence contradiction by A29, A30, A31, A32, FUNCT_1:def 8; :: thesis:

end;

now

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A33: ( Di = product c1 & Di1 = product c2 ) ; :: thesis:
A34: c1 = b2 +* i,{(F . j)} by A21, A23, A33, PUA2MSS1:2;
then c1 . (indx b2) = b2 . (indx b2) by A4, FUNCT_7:34;
then A35: not c1 . (indx b2) is trivial by PENCIL_1:def 21;
then A36: indx c1 = indx b2 by PENCIL_1:def 21;
A37: c2 = b2 +* i,{(F . (j + 1))} by A21, A25, A33, PUA2MSS1:2;
then c2 . (indx b2) = b2 . (indx b2) by A4, FUNCT_7:34;
then not c2 . (indx b2) is trivial by PENCIL_1:def 21;
hence indx c1 = indx c2 by A36, PENCIL_1:def 21; :: thesis:
take r = i; :: thesis:
thus r <> indx c1 by A4, A35, 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 A38: j <> r ; :: thesis:
hence c1 . j = b2 . j by A34, FUNCT_7:34
.= c2 . j by A37, A38, FUNCT_7:34 ;
:: 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 A39: ( c1 . r = {p1} & c2 . r = {p2} ) ; :: thesis:
c1 . r = {(F . j)} by A3, A34, FUNCT_7:33;
then A40: F . j = p1 by A39, ZFMISC_1:6;
c2 . r = {(F . (j + 1))} by A3, A37, FUNCT_7:33;
then F . (j + 1) = p2 by A39, ZFMISC_1:6;
hence p1,p2 are_collinear by A9, A10, A20, A40; :: thesis:

end;

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

end;