let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I
for p, q being Point of () st p <> q holds
( p,q are_collinear iff 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 ) ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: for p, q being Point of () st p <> q holds
( p,q are_collinear iff 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 ) ) )

let p, q be Point of (); :: thesis: ( p <> q implies ( p,q are_collinear iff 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 ) ) ) )

assume A1: p <> q ; :: thesis: ( p,q are_collinear iff 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 ) ) )

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: ( ( 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 ) ) ) implies p,q are_collinear )
proof
assume p,q are_collinear ; :: thesis: 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 ) )

then consider l being Block of () such that
A2: {p,q} c= l by ;
let p1, q1 be ManySortedSet of I; :: thesis: ( p1 = p & q1 = q implies 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 ) ) )

assume that
A3: p1 = p and
A4: q1 = q ; :: thesis: 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 ) )

A5: q1 in l by ;
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: ( ( 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 ) )

A8: p1 in l by ;
thus for a, b being Point of (A . i) st a = p1 . i & b = q1 . i holds
( a <> b & a,b are_collinear ) :: thesis: for j being Element of I st j <> i holds
p1 . j = q1 . j
proof
reconsider LI = L . (indx L) as Block of (A . (indx L)) by A7;
let a, b be Point of (A . i); :: thesis: ( a = p1 . i & b = q1 . i implies ( a <> b & a,b are_collinear ) )
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 ;
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 ;
assume A11: ( a = p1 . i & b = q1 . i ) ; :: thesis: ( a <> b & a,b are_collinear )
now :: thesis: not a = b
assume A12: a = b ; :: thesis: contradiction
A13: now :: thesis: for o being object st o in dom p1 holds
p1 . o = q1 . o
let o be object ; :: thesis: ( o in dom p1 implies p1 . b1 = q1 . b1 )
assume A14: o in dom p1 ; :: thesis: p1 . b1 = q1 . b1
then reconsider o1 = o as Element of I ;
per cases ( o1 = i or o1 <> i ) ;
suppose o1 = i ; :: thesis: p1 . b1 = q1 . b1
hence p1 . o = q1 . o by ; :: thesis: verum
end;
suppose o1 <> i ; :: thesis: p1 . b1 = q1 . b1
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 ; :: thesis: verum
end;
end;
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: verum
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 ;
then {a,b} c= LI by ;
hence a,b are_collinear by PENCIL_1:def 1; :: thesis: verum
end;
let j be Element of I; :: thesis: ( j <> i implies p1 . j = q1 . j )
assume j <> i ; :: thesis: p1 . j = q1 . j
hence p1 . j = q1 . j by ; :: thesis: verum
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 () . 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 () . 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 ( a = b or ex l being Block of (A . i) st {a,b} c= l ) by ;
suppose a = b ; :: 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 () 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: ( o in dom ({p1} +* (i,l)) implies q1 . o in ({p1} +* (i,l)) . o )
assume A26: o in dom ({p1} +* (i,l)) ; :: thesis: q1 . o in ({p1} +* (i,l)) . o
then reconsider o1 = o as Element of I ;
per cases ( o1 = i or o1 <> i ) ;
suppose A27: o1 = i ; :: thesis: q1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = l by ;
hence q1 . o in ({p1} +* (i,l)) . o by ; :: thesis: verum
end;
suppose A28: o1 <> i ; :: thesis: q1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32;
then ({p1} +* (i,l)) . o = {(p1 . o)} by ;
then ({p1} +* (i,l)) . o = {(q1 . o1)} by ;
hence q1 . o in ({p1} +* (i,l)) . o by TARSKI:def 1; :: thesis: verum
end;
end;
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: ( o in dom ({p1} +* (i,l)) implies p1 . o in ({p1} +* (i,l)) . o )
assume A30: o in dom ({p1} +* (i,l)) ; :: thesis: p1 . o in ({p1} +* (i,l)) . o
per cases ( o = i or o <> i ) ;
suppose A31: o = i ; :: thesis: p1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = l by ;
hence p1 . o in ({p1} +* (i,l)) . o by ; :: thesis: verum
end;
suppose o <> i ; :: thesis: p1 . o in ({p1} +* (i,l)) . o
then ({p1} +* (i,l)) . o = {p1} . o by FUNCT_7:32;
then ({p1} +* (i,l)) . o = {(p1 . o)} by ;
hence p1 . o in ({p1} +* (i,l)) . o by TARSKI:def 1; :: thesis: verum
end;
end;
end;
dom q1 = dom ({p1} +* (i,l)) by ;
then A32: q in L by ;
dom p1 = dom ({p1} +* (i,l)) by ;
then p in L by ;
then {p,q} c= L by ;
hence p,q are_collinear by PENCIL_1:def 1; :: thesis: verum
end;
end;