let I be non empty set ; :: thesis:
let A be PLS-yielding ManySortedSet of I; :: thesis:
let p, q be Point of (Segre_Product A); :: thesis:
assume A1: p <> q ; :: thesis:
thus ( p,q are_collinear implies for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) ) :: thesis:

proof

assume p,q are_collinear ; :: thesis:
then consider l being Block of (Segre_Product A) such that
A2: {p,q} c= l by A1, PENCIL_1:def 1;
let p1, q1 be ManySortedSet of I; :: thesis:
assume that
A3: p1 = p and
A4: q1 = q ; :: thesis:
A5: q1 in l by A2, A4, ZFMISC_1:32;
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A6: l = product L and
A7: L . (indx L) is Block of (A . (indx L)) by PENCIL_1:24;
take i = indx L; :: thesis:
A8: p1 in l by A2, A3, ZFMISC_1:32;
thus for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) :: thesis:

proof

reconsider LI = L . (indx L) as Block of (A . (indx L)) by A7;
let a, b be Point of (A . i); :: thesis:
A9: ex p0 being Function st
( p0 = p1 & dom p0 = dom L & ( for o being object st o in dom L holds
p0 . o in L . o ) ) by A6, A8, CARD_3:def 5;
A10: ex q0 being Function st
( q0 = q1 & dom q0 = dom L & ( for o being object st o in dom L holds
q0 . o in L . o ) ) by A6, A5, CARD_3:def 5;
assume A11: ( a = p1 . i & b = q1 . i ) ; :: thesis:

now :: thesis:

assume A12: a = b ; :: thesis:

A13: now :: thesis:

let o be object ; :: thesis:
assume A14: o in dom p1 ; :: thesis:
then reconsider o1 = o as Element of I ;

per cases ;

suppose o1 = i ; :: thesis:

hence p1 . o = q1 . o by A11, A12; :: thesis:

end;

suppose o1 <> i ; :: thesis:

then L . o1 is 1 -element by PENCIL_1:12;
then consider s being object such that
A15: L . o1 = {s} by ZFMISC_1:131;
p1 . o in {s} by A9, A14, A15;
then A16: p1 . o = s by TARSKI:def 1;
q1 . o in {s} by A9, A10, A14, A15;
hence p1 . o = q1 . o by A16, TARSKI:def 1; :: thesis:

end;

dom p1 = I by PARTFUN1:def 2
.= dom q1 by PARTFUN1:def 2 ;
hence contradiction by A1, A3, A4, A13, FUNCT_1:2; :: thesis:

end;

hence a <> b ; :: thesis:
A17: dom L = I by PARTFUN1:def 2;
then A18: q1 . i in LI by A10;
p1 . i in LI by A9, A17;
then {a,b} c= LI by A11, A18, ZFMISC_1:32;
hence a,b are_collinear by PENCIL_1:def 1; :: thesis:

end;

let j be Element of I; :: thesis:
assume j <> i ; :: thesis:
hence p1 . j = q1 . j by A6, A8, A5, PENCIL_1:23; :: thesis:

end;

reconsider p1 = p, q1 = q as Element of Carrier A by Th6;
assume for p1, q1 being ManySortedSet of I st p1 = p & q1 = q holds
ex i being Element of I st
( ( for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) ) & ( for j being Element of I st j <> i holds
p1 . j = q1 . j ) ) ; :: thesis:
then consider i being Element of I such that
A19: for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) and
A20: for j being Element of I st j <> i holds
p1 . j = q1 . j ;
q1 . i is Element of (Carrier A) . i by PBOOLE:def 14;
then q1 . i is Element of [#] (A . i) by Th7;
then reconsider b = q1 . i as Point of (A . i) ;
p1 . i is Element of (Carrier A) . i by PBOOLE:def 14;
then p1 . i is Element of [#] (A . i) by Th7;
then reconsider a = p1 . i as Point of (A . i) ;
A21: a,b are_collinear by A19;

per cases by A21, PENCIL_1:def 1;

suppose a = b ; :: thesis:

hence p,q are_collinear by A19; :: thesis:

end;

suppose ex l being Block of (A . i) st {a,b} c= l ; :: thesis:

then consider l being Block of (A . i) such that
A22: {a,b} c= l ;
reconsider L = product ({p1} +* (i,l)) as Block of (Segre_Product A) by Th16;
A23: dom ({p1} +* (i,l)) = I by PARTFUN1:def 2;
then A24: dom {p1} = dom ({p1} +* (i,l)) by PARTFUN1:def 2;
A25: for o being object st o in dom ({p1} +* (i,l)) holds
q1 . o in ({p1} +* (i,l)) . o

proof

let o be object ; :: thesis:
assume A26: o in dom ({p1} +* (i,l)) ; :: thesis:
then reconsider o1 = o as Element of I ;

per cases ;

suppose A27: o1 = i ; :: thesis:

then ({p1} +* (i,l)) . o = l by A24, A26, FUNCT_7:31;
hence q1 . o in ({p1} +* (i,l)) . o by A22, A27, ZFMISC_1:32; :: thesis:

end;

suppose A28: o1 <> i ; :: thesis:

then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32;
then ({p1} +* (i,l)) . o = {(p1 . o)} by A26, PZFMISC1:def 1;
then ({p1} +* (i,l)) . o = {(q1 . o1)} by A20, A28;
hence q1 . o in ({p1} +* (i,l)) . o by TARSKI:def 1; :: thesis:

end;

A29: for o being object st o in dom ({p1} +* (i,l)) holds
p1 . o in ({p1} +* (i,l)) . o

proof

let o be object ; :: thesis:
assume A30: o in dom ({p1} +* (i,l)) ; :: thesis:

per cases ;

suppose A31: o = i ; :: thesis:

then ({p1} +* (i,l)) . o = l by A24, A30, FUNCT_7:31;
hence p1 . o in ({p1} +* (i,l)) . o by A22, A31, ZFMISC_1:32; :: thesis:

end;

suppose o <> i ; :: thesis:

then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32;
then ({p1} +* (i,l)) . o = {(p1 . o)} by A30, PZFMISC1:def 1;
hence p1 . o in ({p1} +* (i,l)) . o by TARSKI:def 1; :: thesis:

end;

dom q1 = dom ({p1} +* (i,l)) by A23, PARTFUN1:def 2;
then A32: q in L by A25, CARD_3:def 5;
dom p1 = dom ({p1} +* (i,l)) by A23, PARTFUN1:def 2;
then p in L by A29, CARD_3:def 5;
then {p,q} c= L by A32, ZFMISC_1:32;
hence p,q are_collinear by PENCIL_1:def 1; :: thesis:

end;