let I be non empty set ; :: thesis:
let A be PLS-yielding ManySortedSet of ; :: 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 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;
consider L being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A3: ( l = product L & L . (indx L) is Block of (A . (indx L)) ) by PENCIL_1:24;
let p1, q1 be ManySortedSet of ; :: thesis:
assume A4: ( p1 = p & q1 = q ) ; :: thesis:
then A5: ( p1 in l & q1 in l ) by A2, ZFMISC_1:38;
take i = indx L; :: thesis:
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

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

now

assume A9: a = b ; :: thesis:
A10: dom p1 = I by PARTFUN1:def 4
.= dom q1 by PARTFUN1:def 4 ;

now

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

per cases ;

suppose o1 = i ; :: thesis:

hence p1 . o = q1 . o by A6, A9; :: thesis:

end;

suppose o1 <> i ; :: thesis:

then ( not L . o1 is empty & L . o1 is trivial ) by PENCIL_1:12;
then consider s being set such that
A12: L . o1 = {s} by REALSET1:def 4;
( p1 . o in {s} & q1 . o in {s} ) by A7, A8, A11, A12;
then ( p1 . o = s & q1 . o = s ) by TARSKI:def 1;
hence p1 . o = q1 . o ; :: thesis:

end;

hence contradiction by A1, A4, A10, FUNCT_1:9; :: thesis:

end;

hence a <> b ; :: thesis:
dom L = I by PARTFUN1:def 4;
then ( p1 . i in LI & q1 . i in LI ) by A7, A8;
then {a,b} c= LI by A6, ZFMISC_1:38;
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 A3, A5, PENCIL_1:23; :: thesis:

end;

assume A13: for p1, q1 being ManySortedSet of 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:
reconsider p1 = p, q1 = q as Element of Carrier A by Th6;
consider i being Element of I such that
A14: ( ( 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 ) ) by A13;
p1 . i is Element of (Carrier A) . i by PBOOLE:def 17;
then p1 . i is Element of [#] (A . i) by Th7;
then reconsider a = p1 . i as Point of (A . i) ;
q1 . i is Element of (Carrier A) . i by PBOOLE:def 17;
then q1 . i is Element of [#] (A . i) by Th7;
then reconsider b = q1 . i as Point of (A . i) ;
A15: a,b are_collinear by A14;

per cases by A15, PENCIL_1:def 1;

suppose a = b ; :: thesis:

hence p,q are_collinear by A14; :: 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
A16: {a,b} c= l ;
reconsider L = product ({p1} +* i,l) as Block of (Segre_Product A) by Th16;
A17: dom ({p1} +* i,l) = I by PARTFUN1:def 4;
then A18: dom {p1} = dom ({p1} +* i,l) by PARTFUN1:def 4;
A19: dom p1 = dom ({p1} +* i,l) by A17, PARTFUN1:def 4;
for o being set st o in dom ({p1} +* i,l) holds
p1 . o in ({p1} +* i,l) . o

proof

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

per cases ;

suppose A21: o = i ; :: thesis:

then ({p1} +* i,l) . o = l by A18, A20, FUNCT_7:33;
hence p1 . o in ({p1} +* i,l) . o by A16, A21, ZFMISC_1:38; :: thesis:

end;

suppose o <> i ; :: thesis:

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

end;

then A22: p in L by A19, CARD_3:def 5;
A23: dom q1 = dom ({p1} +* i,l) by A17, PARTFUN1:def 4;
for o being set st o in dom ({p1} +* i,l) holds
q1 . o in ({p1} +* i,l) . o

proof

let o be set ; :: thesis:
assume A24: o in dom ({p1} +* i,l) ; :: thesis:
then reconsider o1 = o as Element of I by PARTFUN1:def 4;

per cases ;

suppose A25: o1 = i ; :: thesis:

then ({p1} +* i,l) . o = l by A18, A24, FUNCT_7:33;
hence q1 . o in ({p1} +* i,l) . o by A16, A25, ZFMISC_1:38; :: thesis:

end;

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

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

end;

then q in L by A23, CARD_3:def 5;
then {p,q} c= L by A22, ZFMISC_1:38;
hence p,q are_collinear by PENCIL_1:def 1; :: thesis:

end;