let I be non empty set ; :: thesis:
let A be PLS-yielding ManySortedSet of ; :: thesis:
let B1, B2 be Segre-Coset of A; :: thesis:
assume A1: B1 misses B2 ; :: thesis:
thus ( B1 '||' B2 implies for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) ) :: thesis:

proof

assume A2: B1 '||' B2 ; :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A3: ( B1 = product b1 & B2 = product b2 ) ; :: thesis:
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A4: ( B1 = product L1 & L1 . (indx L1) = [#] (A . (indx L1)) ) by PENCIL_2:def 2;
consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A5: ( B2 = product L2 & L2 . (indx L2) = [#] (A . (indx L2)) ) by PENCIL_2:def 2;
A6: b1 = L1 by A3, A4, PUA2MSS1:2;
A7: b2 = L2 by A3, A5, PUA2MSS1:2;
thus A8: indx b1 = indx b2 :: thesis:

proof

assume indx b1 <> indx b2 ; :: thesis:
then ( not b2 . (indx b1) is empty & b2 . (indx b1) is trivial ) by PENCIL_1:12;
then consider c2 being set such that
A9: b2 . (indx b1) = {c2} by REALSET1:def 4;
consider p0 being set such that
A10: p0 in B1 by A3, XBOOLE_0:def 1;
reconsider p0 = p0 as Point of (Segre_Product A) by A10;
reconsider p = p0 as Element of Carrier A by Th6;
consider bl being Block of (A . (indx b1));
A11: 2 c= card bl by PENCIL_1:def 6;
bl in the topology of (A . (indx b1)) ;
then card bl c= card the carrier of (A . (indx b1)) by CARD_1:27;
then 2 c= card the carrier of (A . (indx b1)) by A11, XBOOLE_1:1;
then consider a being set such that
A12: ( a in the carrier of (A . (indx b1)) & a <> c2 ) by PENCIL_1:3;
reconsider a = a as Point of (A . (indx b1)) by A12;
reconsider x = p +* (indx b1),a as Point of (Segre_Product A) by PENCIL_1:25;
reconsider x1 = x as Element of Carrier A by Th6;
A13: dom x1 = I by PARTFUN1:def 4
.= dom b1 by PARTFUN1:def 4 ;

now

let i be set ; :: thesis:
assume A14: i in dom x1 ; :: thesis:
then i in I by PARTFUN1:def 4;
then A15: i in dom p by PARTFUN1:def 4;

per cases ;

suppose A16: i = indx b1 ; :: thesis:

then x1 . i = a by A15, FUNCT_7:33;
hence x1 . i in b1 . i by A4, A6, A16; :: thesis:

end;

suppose A17: i <> indx b1 ; :: thesis:

consider f being Function such that
A18: ( f = p & dom f = dom b1 & ( for a being set st a in dom b1 holds
f . a in b1 . a ) ) by A3, A10, CARD_3:def 5;
x1 . i = p . i by A17, FUNCT_7:34;
hence x1 . i in b1 . i by A13, A14, A18; :: thesis:

end;

then A19: x in B1 by A3, A13, CARD_3:def 5;
then consider y being Point of (Segre_Product A) such that
A20: ( y in B2 & x,y are_collinear ) by A2, Def2;
reconsider y1 = y as Element of Carrier A by Th6;

per cases ;

suppose y = x ; :: thesis:

then y in B1 /\ B2 by A19, A20, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

suppose y <> x ; :: thesis:

then consider i0 being Element of I such that
A21: ( ( for a, b being Point of (A . i0) st a = x1 . i0 & b = y1 . i0 holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i0 holds
x1 . j = y1 . j ) ) by A20, Th17;
A22: dom y1 = I by PARTFUN1:def 4
.= dom b1 by PARTFUN1:def 4 ;

now

let i be set ; :: thesis:
assume A23: i in dom y1 ; :: thesis:
then reconsider i5 = i as Element of I by PARTFUN1:def 4;

per cases ;

suppose A24: i = indx b1 ; :: thesis:

reconsider i1 = i as Element of I by A23, PARTFUN1:def 4;
y1 . i1 is Element of (Carrier A) . i1 by PBOOLE:def 17;
then y1 . i1 is Element of [#] (A . i1) by Th7;
hence y1 . i in b1 . i by A4, A6, A24; :: thesis:

end;

suppose A25: i <> indx b1 ; :: thesis:

consider f being Function such that
A26: ( f = p & dom f = dom b1 & ( for a being set st a in dom b1 holds
f . a in b1 . a ) ) by A3, A10, CARD_3:def 5;
dom p = I by PARTFUN1:def 4;
then A27: x1 . (indx b1) = a by FUNCT_7:33;
consider g being Function such that
A28: ( g = y1 & dom g = dom b2 & ( for a being set st a in dom b2 holds
g . a in b2 . a ) ) by A3, A20, CARD_3:def 5;
dom b2 = I by PARTFUN1:def 4;
then y1 . (indx b1) in b2 . (indx b1) by A28;
then y1 . (indx b1) = c2 by A9, TARSKI:def 1;
then i0 = indx b1 by A12, A21, A27;
then A29: y1 . i5 = x1 . i5 by A21, A25;
x1 . i = p . i by A25, FUNCT_7:34;
hence y1 . i in b1 . i by A22, A23, A26, A29; :: thesis:

end;

then y in B1 by A3, A22, CARD_3:def 5;
then y in B1 /\ B2 by A20, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

thus ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) :: thesis:

proof

consider x being set such that
A30: x in B1 by A3, XBOOLE_0:def 1;
reconsider x = x as Point of (Segre_Product A) by A30;
reconsider x1 = x as Element of Carrier A by Th6;
consider y being Point of (Segre_Product A) such that
A31: ( y in B2 & x,y are_collinear ) by A2, A30, Def2;
reconsider y1 = y as Element of Carrier A by Th6;

now

assume x = y ; :: thesis:
then B1 /\ B2 <> {} by A30, A31, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

then consider r being Element of I such that
A32: ( ( for a, b being Point of (A . r) st a = x1 . r & b = y1 . r holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> r holds
x1 . j = y1 . j ) ) by A31, Th17;
take r ; :: thesis:

now

assume A33: r = indx b1 ; :: thesis:
A34: dom y1 = I by PARTFUN1:def 4
.= dom b1 by PARTFUN1:def 4 ;

now

let o be set ; :: thesis:
assume A35: o in dom b1 ; :: thesis:
then reconsider o1 = o as Element of I by PARTFUN1:def 4;

per cases ;

suppose A36: o1 = r ; :: thesis:

y1 . o1 is Element of (Carrier A) . o1 by PBOOLE:def 17;
then y1 . o1 is Element of [#] (A . o1) by Th7;
hence y1 . o in b1 . o by A4, A6, A33, A36; :: thesis:

end;

suppose A37: o1 <> r ; :: thesis:

then ( b1 . o1 is trivial & not b1 . o1 is empty ) by A33, PENCIL_1:12;
then consider c being set such that
A38: b1 . o1 = {c} by REALSET1:def 4;
x1 . o1 in b1 . o1 by A3, A30, A35, CARD_3:18;
then c = x1 . o1 by A38, TARSKI:def 1
.= y1 . o1 by A32, A37 ;
hence y1 . o in b1 . o by A38, TARSKI:def 1; :: thesis:

end;

then y1 in B1 by A3, A34, CARD_3:18;
then B1 /\ B2 <> {} by A31, XBOOLE_0:def 4;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis:

end;

hence r <> indx b1 ; :: thesis:
thus for i being Element of I st i <> r holds
b1 . i = b2 . i :: thesis:

proof

let i be Element of I; :: thesis:
assume A39: i <> r ; :: thesis:

per cases ;

suppose i = indx b1 ; :: thesis:

hence b1 . i = b2 . i by A4, A5, A6, A7, A8; :: thesis:

end;

suppose A40: i <> indx b1 ; :: thesis:

then ( b1 . i is trivial & not b1 . i is empty ) by PENCIL_1:12;
then consider c being set such that
A41: b1 . i = {c} by REALSET1:def 4;
( b2 . i is trivial & not b2 . i is empty ) by A8, A40, PENCIL_1:12;
then consider d being set such that
A42: b2 . i = {d} by REALSET1:def 4;
dom b1 = I by PARTFUN1:def 4;
then x1 . i in b1 . i by A3, A30, CARD_3:18;
then A43: c = x1 . i by A41, TARSKI:def 1
.= y1 . i by A32, A39 ;
dom b2 = I by PARTFUN1:def 4;
then y1 . i in b2 . i by A3, A31, CARD_3:18;
hence b1 . i = b2 . i by A41, A42, A43, TARSKI:def 1; :: thesis:

end;

let c1, c2 be Point of (A . r); :: thesis:
assume A44: ( b1 . r = {c1} & b2 . r = {c2} ) ; :: thesis:
dom L1 = I by PARTFUN1:def 4;
then x1 . r in b1 . r by A4, A6, A30, CARD_3:18;
then A45: c1 = x1 . r by A44, TARSKI:def 1;
dom L2 = I by PARTFUN1:def 4;
then y1 . r in b2 . r by A5, A7, A31, CARD_3:18;
then c2 = y1 . r by A44, TARSKI:def 1;
hence c1,c2 are_collinear by A32, A45; :: thesis:

end;

assume A46: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st B1 = product b1 & B2 = product b2 holds
( indx b1 = indx b2 & ex r being Element of I st
( r <> indx b1 & ( for i being Element of I st i <> r holds
b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds
c1,c2 are_collinear ) ) ) ; :: thesis:
consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A47: ( B1 = product L1 & L1 . (indx L1) = [#] (A . (indx L1)) ) by PENCIL_2:def 2;
consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A48: ( B2 = product L2 & L2 . (indx L2) = [#] (A . (indx L2)) ) by PENCIL_2:def 2;
A49: indx L1 = indx L2 by A46, A47, A48;
consider r being Element of I such that
A50: ( r <> indx L1 & ( for i being Element of I st i <> r holds
L1 . i = L2 . i ) & ( for c1, c2 being Point of (A . r) st L1 . r = {c1} & L2 . r = {c2} holds
c1,c2 are_collinear ) ) by A46, A47, A48;
( not L1 . r is empty & L1 . r is trivial ) by A50, PENCIL_1:12;
then consider c1 being set such that
A51: L1 . r = {c1} by REALSET1:def 4;
L1 c= Carrier A by PBOOLE:def 23;
then L1 . r c= (Carrier A) . r by PBOOLE:def 5;
then {c1} c= [#] (A . r) by A51, Th7;
then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:37;
( not L2 . r is empty & L2 . r is trivial ) by A49, A50, PENCIL_1:12;
then consider c2 being set such that
A52: L2 . r = {c2} by REALSET1:def 4;
L2 c= Carrier A by PBOOLE:def 23;
then L2 . r c= (Carrier A) . r by PBOOLE:def 5;
then {c2} c= [#] (A . r) by A52, Th7;
then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:37;

A53: now

assume A54: c1 = c2 ; :: thesis:
A55: dom L1 = I by PARTFUN1:def 4
.= dom L2 by PARTFUN1:def 4 ;

now

let s be set ; :: thesis:
assume s in dom L1 ; :: thesis:
then reconsider s1 = s as Element of I by PARTFUN1:def 4;

per cases ;

suppose s1 = r ; :: thesis:

hence L1 . s = L2 . s by A51, A52, A54; :: thesis:

end;

suppose s1 <> r ; :: thesis:

hence L1 . s = L2 . s by A50; :: thesis:

end;

then L1 = L2 by A55, FUNCT_1:9;
then B1 /\ B1 = {} by A1, A47, A48, XBOOLE_0:def 7;
hence contradiction by A47; :: thesis:

end;

c1,c2 are_collinear by A50, A51, A52;
then consider bb being Block of (A . r) such that
A56: {c1,c2} c= bb by A53, PENCIL_1:def 1;
let x be Point of (Segre_Product A); :: according to PENCIL_3:def 2 :: thesis:
assume A57: x in B1 ; :: thesis:
reconsider x1 = x as Element of Carrier A by Th6;
consider x2 being Function such that
A58: ( x2 = x & dom x2 = dom L1 & ( for o being set st o in dom L1 holds
x2 . o in L1 . o ) ) by A47, A57, CARD_3:def 5;
reconsider y = x1 +* r,c2 as Point of (Segre_Product A) by PENCIL_1:25;
take y ; :: thesis:
reconsider y1 = y as ManySortedSet of ;
A59: dom y1 = I by PARTFUN1:def 4
.= dom L2 by PARTFUN1:def 4 ;

now

let a be set ; :: thesis:
assume a in dom L2 ; :: thesis:
then reconsider a1 = a as Element of I by PARTFUN1:def 4;

per cases ;

suppose A60: a1 = r ; :: thesis:

dom x1 = I by PARTFUN1:def 4;
then y1 . a = c2 by A60, FUNCT_7:33;
hence y1 . a in L2 . a by A52, A60, TARSKI:def 1; :: thesis:

end;

suppose A61: a1 <> r ; :: thesis:

A62: dom x1 = I by PARTFUN1:def 4;
y1 . a1 = x1 . a1 by A61, FUNCT_7:34;
then y1 . a1 in L1 . a1 by A58, A62;
hence y1 . a in L2 . a by A50, A61; :: thesis:

end;

hence y in B2 by A48, A59, CARD_3:def 5; :: thesis:
reconsider B = product ({x1} +* r,bb) as Block of (Segre_Product A) by Th16;
A63: dom x1 = I by PARTFUN1:def 4
.= dom ({x1} +* r,bb) by PARTFUN1:def 4 ;

now

let s be set ; :: thesis:
assume A64: s in dom x1 ; :: thesis:
then A65: s in I by PARTFUN1:def 4;
then A66: s in dom {x1} by PARTFUN1:def 4;

per cases ;

suppose A67: s = r ; :: thesis:

x1 . s in L1 . s by A58, A64;
then A68: x1 . s = c1 by A51, A67, TARSKI:def 1;
bb = ({x1} +* r,bb) . s by A66, A67, FUNCT_7:33;
hence x1 . s in ({x1} +* r,bb) . s by A56, A68, ZFMISC_1:38; :: thesis:

end;

suppose s <> r ; :: thesis:

then {x1} . s = ({x1} +* r,bb) . s by FUNCT_7:34;
then {(x1 . s)} = ({x1} +* r,bb) . s by A65, PZFMISC1:def 1;
hence x1 . s in ({x1} +* r,bb) . s by TARSKI:def 1; :: thesis:

end;

then A69: x in B by A63, CARD_3:def 5;
A70: dom y1 = I by PARTFUN1:def 4
.= dom ({x1} +* r,bb) by PARTFUN1:def 4 ;

now

let s be set ; :: thesis:
assume s in dom y1 ; :: thesis:
then A71: s in I by PARTFUN1:def 4;
then A72: ( s in dom {x1} & s in dom x1 ) by PARTFUN1:def 4;

per cases ;

suppose A73: s = r ; :: thesis:

then A74: y1 . s = c2 by A72, FUNCT_7:33;
bb = ({x1} +* r,bb) . s by A72, A73, FUNCT_7:33;
hence y1 . s in ({x1} +* r,bb) . s by A56, A74, ZFMISC_1:38; :: thesis:

end;

suppose A75: s <> r ; :: thesis:

then A76: y1 . s = x1 . s by FUNCT_7:34;
{x1} . s = ({x1} +* r,bb) . s by A75, FUNCT_7:34;
then {(x1 . s)} = ({x1} +* r,bb) . s by A71, PZFMISC1:def 1;
hence y1 . s in ({x1} +* r,bb) . s by A76, TARSKI:def 1; :: thesis:

end;

then y in B by A70, CARD_3:def 5;
then {x,y} c= B by A69, ZFMISC_1:38;
hence x,y are_collinear by PENCIL_1:def 1; :: thesis: