let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I

for p, q being Point of (Segre_Product A) 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 (Segre_Product A) 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 (Segre_Product A); :: 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 )

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: p,q are_collinear

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;

for p, q being Point of (Segre_Product A) 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 (Segre_Product A) 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 (Segre_Product A); :: 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

reconsider p1 = p, q1 = q as Element of Carrier A by Th6;
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 (Segre_Product A) such that

A2: {p,q} c= l by A1, PENCIL_1:def 1;

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 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: ( ( 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 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: for j being Element of I st j <> i holds

p1 . j = q1 . j

assume j <> i ; :: thesis: p1 . j = q1 . j

hence p1 . j = q1 . j by A6, A8, A5, PENCIL_1:23; :: thesis: verum

end;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 (Segre_Product A) such that

A2: {p,q} c= l by A1, PENCIL_1:def 1;

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 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: ( ( 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 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: for j being Element of I st j <> i holds

p1 . j = q1 . j

proof

let j be Element of I; :: thesis: ( j <> i implies p1 . j = q1 . j )
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 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: ( a <> b & a,b are_collinear )

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: verum

end;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 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: ( a <> b & a,b are_collinear )

now :: thesis: not a = b

hence
a <> b
; :: thesis: a,b are_collinear assume A12:
a = b
; :: thesis: contradiction

.= dom q1 by PARTFUN1:def 2 ;

hence contradiction by A1, A3, A4, A13, FUNCT_1:2; :: thesis: verum

end;A13: now :: thesis: for o being object st o in dom p1 holds

p1 . o = q1 . o

dom p1 =
I
by PARTFUN1:def 2
p1 . o = q1 . o

let o be object ; :: thesis: ( o in dom p1 implies p1 . b_{1} = q1 . b_{1} )

assume A14: o in dom p1 ; :: thesis: p1 . b_{1} = q1 . b_{1}

then reconsider o1 = o as Element of I ;

end;assume A14: o in dom p1 ; :: thesis: p1 . b

then reconsider o1 = o as Element of I ;

per cases
( o1 = i or o1 <> i )
;

end;

suppose
o1 <> i
; :: thesis: p1 . b_{1} = q1 . b_{1}

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: verum

end;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: verum

.= dom q1 by PARTFUN1:def 2 ;

hence contradiction by A1, A3, A4, A13, FUNCT_1:2; :: thesis: verum

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: verum

assume j <> i ; :: thesis: p1 . j = q1 . j

hence p1 . j = q1 . j by A6, A8, A5, PENCIL_1:23; :: thesis: verum

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: p,q are_collinear

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
( a = b or ex l being Block of (A . i) st {a,b} c= l )
by A21, PENCIL_1:def 1;

end;

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

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

p1 . o in ({p1} +* (i,l)) . o

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: verum

end;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

A29:
for o being object st o in dom ({p1} +* (i,l)) holds
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 ;

end;assume A26: o in dom ({p1} +* (i,l)) ; :: thesis: q1 . o in ({p1} +* (i,l)) . o

then reconsider o1 = o as Element of I ;

p1 . o in ({p1} +* (i,l)) . o

proof

dom q1 = dom ({p1} +* (i,l))
by A23, PARTFUN1:def 2;
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

end;assume A30: o in dom ({p1} +* (i,l)) ; :: thesis: p1 . o in ({p1} +* (i,l)) . o

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: verum