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

for B1, B2 being Segre-Coset of A st B1 misses B2 holds

( B1 '||' B2 iff 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 ) ) ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds

( B1 '||' B2 iff 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 ) ) ) )

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 misses B2 implies ( B1 '||' B2 iff 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 ) ) ) ) )

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A1: B1 = product L1 and

L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

assume A2: B1 misses B2 ; :: thesis: ( B1 '||' B2 iff 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 ) ) ) )

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: ( ( 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 ) ) ) ) implies B1 '||' B2 )

A52: B2 = product L2 and

L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;

assume A53: 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: B1 '||' B2

then consider r being Element of I such that

A54: r <> indx L1 and

A55: for i being Element of I st i <> r holds

L1 . i = L2 . i and

A56: for c1, c2 being Point of (A . r) st L1 . r = {c1} & L2 . r = {c2} holds

c1,c2 are_collinear by A1, A52;

indx L1 = indx L2 by A53, A1, A52;

then L2 . r is 1 -element by A54, PENCIL_1:12;

then consider c2 being object such that

A57: L2 . r = {c2} by ZFMISC_1:131;

L2 c= Carrier A by PBOOLE:def 18;

then L2 . r c= (Carrier A) . r ;

then {c2} c= [#] (A . r) by A57, Th7;

then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:31;

L1 . r is 1 -element by A54, PENCIL_1:12;

then consider c1 being object such that

A58: L1 . r = {c1} by ZFMISC_1:131;

L1 c= Carrier A by PBOOLE:def 18;

then L1 . r c= (Carrier A) . r ;

then {c1} c= [#] (A . r) by A58, Th7;

then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;

then consider bb being Block of (A . r) such that

A62: {c1,c2} c= bb by A59, PENCIL_1:def 1;

let x be Point of (Segre_Product A); :: according to PENCIL_3:def 2 :: thesis: ( x in B1 implies ex y being Point of (Segre_Product A) st

( y in B2 & x,y are_collinear ) )

reconsider x1 = x as Element of Carrier A by Th6;

reconsider y = x1 +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25;

reconsider y1 = y as ManySortedSet of I ;

assume x in B1 ; :: thesis: ex y being Point of (Segre_Product A) st

( y in B2 & x,y are_collinear )

then A63: ex x2 being Function st

( x2 = x & dom x2 = dom L1 & ( for o being object st o in dom L1 holds

x2 . o in L1 . o ) ) by A1, CARD_3:def 5;

dom y1 = I by PARTFUN1:def 2

.= dom L2 by PARTFUN1:def 2 ;

hence y in B2 by A52, A64, CARD_3:def 5; :: thesis: x,y are_collinear

reconsider B = product ({x1} +* (r,bb)) as Block of (Segre_Product A) by Th16;

.= dom ({x1} +* (r,bb)) by PARTFUN1:def 2 ;

then A72: y in B by A67, CARD_3:def 5;

.= dom ({x1} +* (r,bb)) by PARTFUN1:def 2 ;

then x in B by A73, CARD_3:def 5;

then {x,y} c= B by A72, ZFMISC_1:32;

hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum

for B1, B2 being Segre-Coset of A st B1 misses B2 holds

( B1 '||' B2 iff 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 ) ) ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: for B1, B2 being Segre-Coset of A st B1 misses B2 holds

( B1 '||' B2 iff 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 ) ) ) )

let B1, B2 be Segre-Coset of A; :: thesis: ( B1 misses B2 implies ( B1 '||' B2 iff 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 ) ) ) ) )

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A1: B1 = product L1 and

L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

assume A2: B1 misses B2 ; :: thesis: ( B1 '||' B2 iff 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 ) ) ) )

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: ( ( 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 ) ) ) ) implies B1 '||' B2 )

proof

consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
assume A3:
B1 '||' B2
; :: thesis: 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 ) ) )

consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A4: B2 = product L2 and

A5: L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A6: B1 = product L1 and

A7: L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & B2 = product b2 implies ( 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 ) ) ) )

assume that

A8: B1 = product b1 and

A9: B2 = product b2 ; :: thesis: ( 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 ) ) )

A10: b1 = L1 by A8, A6, PUA2MSS1:2;

thus A11: indx b1 = indx b2 :: thesis: 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 ) )

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

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

consider L2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A4: B2 = product L2 and

A5: L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;

consider L1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that

A6: B1 = product L1 and

A7: L1 . (indx L1) = [#] (A . (indx L1)) by PENCIL_2:def 2;

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( B1 = product b1 & B2 = product b2 implies ( 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 ) ) ) )

assume that

A8: B1 = product b1 and

A9: B2 = product b2 ; :: thesis: ( 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 ) ) )

A10: b1 = L1 by A8, A6, PUA2MSS1:2;

thus A11: indx b1 = indx b2 :: thesis: 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 ) )

proof

A32:
b2 = L2
by A9, A4, PUA2MSS1:2;
assume
indx b1 <> indx b2
; :: thesis: contradiction

then b2 . (indx b1) is 1 -element by PENCIL_1:12;

then consider c2 being object such that

A12: b2 . (indx b1) = {c2} by ZFMISC_1:131;

set bl = the Block of (A . (indx b1));

consider p0 being object such that

A13: p0 in B1 by A8, XBOOLE_0:def 1;

reconsider p0 = p0 as Point of (Segre_Product A) by A13;

reconsider p = p0 as Element of Carrier A by Th6;

the Block of (A . (indx b1)) in the topology of (A . (indx b1)) ;

then ( 2 c= card the Block of (A . (indx b1)) & card the Block of (A . (indx b1)) c= card the carrier of (A . (indx b1)) ) by CARD_1:11, PENCIL_1:def 6;

then consider a being object such that

A14: a in the carrier of (A . (indx b1)) and

A15: a <> c2 by PENCIL_1:3, XBOOLE_1:1;

reconsider a = a as Point of (A . (indx b1)) by A14;

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;

A16: dom x1 = I by PARTFUN1:def 2

.= dom b1 by PARTFUN1:def 2 ;

then consider y being Point of (Segre_Product A) such that

A22: y in B2 and

A23: x,y are_collinear by A3;

reconsider y1 = y as Element of Carrier A by Th6;

end;then b2 . (indx b1) is 1 -element by PENCIL_1:12;

then consider c2 being object such that

A12: b2 . (indx b1) = {c2} by ZFMISC_1:131;

set bl = the Block of (A . (indx b1));

consider p0 being object such that

A13: p0 in B1 by A8, XBOOLE_0:def 1;

reconsider p0 = p0 as Point of (Segre_Product A) by A13;

reconsider p = p0 as Element of Carrier A by Th6;

the Block of (A . (indx b1)) in the topology of (A . (indx b1)) ;

then ( 2 c= card the Block of (A . (indx b1)) & card the Block of (A . (indx b1)) c= card the carrier of (A . (indx b1)) ) by CARD_1:11, PENCIL_1:def 6;

then consider a being object such that

A14: a in the carrier of (A . (indx b1)) and

A15: a <> c2 by PENCIL_1:3, XBOOLE_1:1;

reconsider a = a as Point of (A . (indx b1)) by A14;

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;

A16: dom x1 = I by PARTFUN1:def 2

.= dom b1 by PARTFUN1:def 2 ;

now :: thesis: for i being object st i in dom x1 holds

x1 . i in b1 . i

then A21:
x in B1
by A8, A16, CARD_3:def 5;x1 . i in b1 . i

let i be object ; :: thesis: ( i in dom x1 implies x1 . b_{1} in b1 . b_{1} )

assume A17: i in dom x1 ; :: thesis: x1 . b_{1} in b1 . b_{1}

then i in I ;

then A18: i in dom p by PARTFUN1:def 2;

end;assume A17: i in dom x1 ; :: thesis: x1 . b

then i in I ;

then A18: i in dom p by PARTFUN1:def 2;

then consider y being Point of (Segre_Product A) such that

A22: y in B2 and

A23: x,y are_collinear by A3;

reconsider y1 = y as Element of Carrier A by Th6;

per cases
( y = x or y <> x )
;

end;

suppose
y <> x
; :: thesis: contradiction

then consider i0 being Element of I such that

for a, b being Point of (A . i0) st a = x1 . i0 & b = y1 . i0 holds

( a <> b & a,b are_collinear ) and

A24: for j being Element of I st j <> i0 holds

x1 . j = y1 . j by A23, Th17;

A25: dom y1 = I by PARTFUN1:def 2

.= dom b1 by PARTFUN1:def 2 ;

then y in B1 /\ B2 by A22, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;for a, b being Point of (A . i0) st a = x1 . i0 & b = y1 . i0 holds

( a <> b & a,b are_collinear ) and

A24: for j being Element of I st j <> i0 holds

x1 . j = y1 . j by A23, Th17;

A25: dom y1 = I by PARTFUN1:def 2

.= dom b1 by PARTFUN1:def 2 ;

now :: thesis: for i being object st i in dom y1 holds

y1 . i in b1 . i

then
y in B1
by A8, A25, CARD_3:def 5;y1 . i in b1 . i

let i be object ; :: thesis: ( i in dom y1 implies y1 . b_{1} in b1 . b_{1} )

assume A26: i in dom y1 ; :: thesis: y1 . b_{1} in b1 . b_{1}

then reconsider i5 = i as Element of I ;

end;assume A26: i in dom y1 ; :: thesis: y1 . b

then reconsider i5 = i as Element of I ;

per cases
( i = indx b1 or i <> indx b1 )
;

end;

suppose A27:
i = indx b1
; :: thesis: y1 . b_{1} in b1 . b_{1}

reconsider i1 = i as Element of I by A26;

y1 . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;

then y1 . i1 is Element of [#] (A . i1) by Th7;

hence y1 . i in b1 . i by A7, A10, A27; :: thesis: verum

end;y1 . i1 is Element of (Carrier A) . i1 by PBOOLE:def 14;

then y1 . i1 is Element of [#] (A . i1) by Th7;

hence y1 . i in b1 . i by A7, A10, A27; :: thesis: verum

suppose A28:
i <> indx b1
; :: thesis: y1 . b_{1} in b1 . b_{1}

( ex g being Function st

( g = y1 & dom g = dom b2 & ( for a being object st a in dom b2 holds

g . a in b2 . a ) ) & dom b2 = I ) by A9, A22, CARD_3:def 5, PARTFUN1:def 2;

then y1 . (indx b1) in b2 . (indx b1) ;

then A29: y1 . (indx b1) = c2 by A12, TARSKI:def 1;

dom p = I by PARTFUN1:def 2;

then x1 . (indx b1) = a by FUNCT_7:31;

then i0 = indx b1 by A15, A24, A29;

then A30: y1 . i5 = x1 . i5 by A24, A28;

A31: x1 . i = p . i by A28, FUNCT_7:32;

ex f being Function st

( f = p & dom f = dom b1 & ( for a being object st a in dom b1 holds

f . a in b1 . a ) ) by A8, A13, CARD_3:def 5;

hence y1 . i in b1 . i by A25, A26, A30, A31; :: thesis: verum

end;( g = y1 & dom g = dom b2 & ( for a being object st a in dom b2 holds

g . a in b2 . a ) ) & dom b2 = I ) by A9, A22, CARD_3:def 5, PARTFUN1:def 2;

then y1 . (indx b1) in b2 . (indx b1) ;

then A29: y1 . (indx b1) = c2 by A12, TARSKI:def 1;

dom p = I by PARTFUN1:def 2;

then x1 . (indx b1) = a by FUNCT_7:31;

then i0 = indx b1 by A15, A24, A29;

then A30: y1 . i5 = x1 . i5 by A24, A28;

A31: x1 . i = p . i by A28, FUNCT_7:32;

ex f being Function st

( f = p & dom f = dom b1 & ( for a being object st a in dom b1 holds

f . a in b1 . a ) ) by A8, A13, CARD_3:def 5;

hence y1 . i in b1 . i by A25, A26, A30, A31; :: thesis: verum

then y in B1 /\ B2 by A22, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

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

proof

consider x being object such that

A33: x in B1 by A8, XBOOLE_0:def 1;

reconsider x = x as Point of (Segre_Product A) by A33;

consider y being Point of (Segre_Product A) such that

A34: y in B2 and

A35: x,y are_collinear by A3, A33;

reconsider y1 = y as Element of Carrier A by Th6;

reconsider x1 = x as Element of Carrier A by Th6;

x <> y by A2, A33, A34, XBOOLE_0:def 4;

then consider r being Element of I such that

A36: for a, b being Point of (A . r) st a = x1 . r & b = y1 . r holds

( a <> b & a,b are_collinear ) and

A37: for j being Element of I st j <> r holds

x1 . j = y1 . j by A35, Th17;

take r ; :: thesis: ( 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 ) )

b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds

c1,c2 are_collinear ) )

thus for i being Element of I st i <> r holds

b1 . i = b2 . i :: thesis: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds

c1,c2 are_collinear

assume that

A49: b1 . r = {c1} and

A50: b2 . r = {c2} ; :: thesis: c1,c2 are_collinear

dom L2 = I by PARTFUN1:def 2;

then y1 . r in b2 . r by A4, A32, A34, CARD_3:9;

then A51: c2 = y1 . r by A50, TARSKI:def 1;

dom L1 = I by PARTFUN1:def 2;

then x1 . r in b1 . r by A6, A10, A33, CARD_3:9;

then c1 = x1 . r by A49, TARSKI:def 1;

hence c1,c2 are_collinear by A36, A51; :: thesis: verum

end;A33: x in B1 by A8, XBOOLE_0:def 1;

reconsider x = x as Point of (Segre_Product A) by A33;

consider y being Point of (Segre_Product A) such that

A34: y in B2 and

A35: x,y are_collinear by A3, A33;

reconsider y1 = y as Element of Carrier A by Th6;

reconsider x1 = x as Element of Carrier A by Th6;

x <> y by A2, A33, A34, XBOOLE_0:def 4;

then consider r being Element of I such that

A36: for a, b being Point of (A . r) st a = x1 . r & b = y1 . r holds

( a <> b & a,b are_collinear ) and

A37: for j being Element of I st j <> r holds

x1 . j = y1 . j by A35, Th17;

take r ; :: thesis: ( 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 ) )

now :: thesis: not r = indx b1

hence
r <> indx b1
; :: thesis: ( ( for i being Element of I st i <> r holds assume A38:
r = indx b1
; :: thesis: contradiction

.= dom b1 by PARTFUN1:def 2 ;

then y1 in B1 by A8, A39, CARD_3:9;

then B1 /\ B2 <> {} by A34, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

end;A39: now :: thesis: for o being object st o in dom b1 holds

y1 . o in b1 . o

dom y1 =
I
by PARTFUN1:def 2
y1 . o in b1 . o

let o be object ; :: thesis: ( o in dom b1 implies y1 . b_{1} in b1 . b_{1} )

assume A40: o in dom b1 ; :: thesis: y1 . b_{1} in b1 . b_{1}

then reconsider o1 = o as Element of I ;

end;assume A40: o in dom b1 ; :: thesis: y1 . b

then reconsider o1 = o as Element of I ;

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

end;

suppose A41:
o1 = r
; :: thesis: y1 . b_{1} in b1 . b_{1}

y1 . o1 is Element of (Carrier A) . o1
by PBOOLE:def 14;

then y1 . o1 is Element of [#] (A . o1) by Th7;

hence y1 . o in b1 . o by A7, A10, A38, A41; :: thesis: verum

end;then y1 . o1 is Element of [#] (A . o1) by Th7;

hence y1 . o in b1 . o by A7, A10, A38, A41; :: thesis: verum

suppose A42:
o1 <> r
; :: thesis: y1 . b_{1} in b1 . b_{1}

then
b1 . o1 is 1 -element
by A38, PENCIL_1:12;

then consider c being object such that

A43: b1 . o1 = {c} by ZFMISC_1:131;

x1 . o1 in b1 . o1 by A8, A33, A40, CARD_3:9;

then c = x1 . o1 by A43, TARSKI:def 1

.= y1 . o1 by A37, A42 ;

hence y1 . o in b1 . o by A43, TARSKI:def 1; :: thesis: verum

end;then consider c being object such that

A43: b1 . o1 = {c} by ZFMISC_1:131;

x1 . o1 in b1 . o1 by A8, A33, A40, CARD_3:9;

then c = x1 . o1 by A43, TARSKI:def 1

.= y1 . o1 by A37, A42 ;

hence y1 . o in b1 . o by A43, TARSKI:def 1; :: thesis: verum

.= dom b1 by PARTFUN1:def 2 ;

then y1 in B1 by A8, A39, CARD_3:9;

then B1 /\ B2 <> {} by A34, XBOOLE_0:def 4;

hence contradiction by A2; :: thesis: verum

b1 . i = b2 . i ) & ( for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds

c1,c2 are_collinear ) )

thus for i being Element of I st i <> r holds

b1 . i = b2 . i :: thesis: for c1, c2 being Point of (A . r) st b1 . r = {c1} & b2 . r = {c2} holds

c1,c2 are_collinear

proof

let c1, c2 be Point of (A . r); :: thesis: ( b1 . r = {c1} & b2 . r = {c2} implies c1,c2 are_collinear )
let i be Element of I; :: thesis: ( i <> r implies b1 . i = b2 . i )

assume A44: i <> r ; :: thesis: b1 . i = b2 . i

end;assume A44: i <> r ; :: thesis: b1 . i = b2 . i

per cases
( i = indx b1 or i <> indx b1 )
;

end;

suppose A45:
i <> indx b1
; :: thesis: b1 . i = b2 . i

then
b2 . i is 1 -element
by A11, PENCIL_1:12;

then A46: ex d being object st b2 . i = {d} by ZFMISC_1:131;

dom b2 = I by PARTFUN1:def 2;

then A47: y1 . i in b2 . i by A9, A34, CARD_3:9;

b1 . i is 1 -element by A45, PENCIL_1:12;

then consider c being object such that

A48: b1 . i = {c} by ZFMISC_1:131;

dom b1 = I by PARTFUN1:def 2;

then x1 . i in b1 . i by A8, A33, CARD_3:9;

then c = x1 . i by A48, TARSKI:def 1

.= y1 . i by A37, A44 ;

hence b1 . i = b2 . i by A48, A46, A47, TARSKI:def 1; :: thesis: verum

end;then A46: ex d being object st b2 . i = {d} by ZFMISC_1:131;

dom b2 = I by PARTFUN1:def 2;

then A47: y1 . i in b2 . i by A9, A34, CARD_3:9;

b1 . i is 1 -element by A45, PENCIL_1:12;

then consider c being object such that

A48: b1 . i = {c} by ZFMISC_1:131;

dom b1 = I by PARTFUN1:def 2;

then x1 . i in b1 . i by A8, A33, CARD_3:9;

then c = x1 . i by A48, TARSKI:def 1

.= y1 . i by A37, A44 ;

hence b1 . i = b2 . i by A48, A46, A47, TARSKI:def 1; :: thesis: verum

assume that

A49: b1 . r = {c1} and

A50: b2 . r = {c2} ; :: thesis: c1,c2 are_collinear

dom L2 = I by PARTFUN1:def 2;

then y1 . r in b2 . r by A4, A32, A34, CARD_3:9;

then A51: c2 = y1 . r by A50, TARSKI:def 1;

dom L1 = I by PARTFUN1:def 2;

then x1 . r in b1 . r by A6, A10, A33, CARD_3:9;

then c1 = x1 . r by A49, TARSKI:def 1;

hence c1,c2 are_collinear by A36, A51; :: thesis: verum

A52: B2 = product L2 and

L2 . (indx L2) = [#] (A . (indx L2)) by PENCIL_2:def 2;

assume A53: 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: B1 '||' B2

then consider r being Element of I such that

A54: r <> indx L1 and

A55: for i being Element of I st i <> r holds

L1 . i = L2 . i and

A56: for c1, c2 being Point of (A . r) st L1 . r = {c1} & L2 . r = {c2} holds

c1,c2 are_collinear by A1, A52;

indx L1 = indx L2 by A53, A1, A52;

then L2 . r is 1 -element by A54, PENCIL_1:12;

then consider c2 being object such that

A57: L2 . r = {c2} by ZFMISC_1:131;

L2 c= Carrier A by PBOOLE:def 18;

then L2 . r c= (Carrier A) . r ;

then {c2} c= [#] (A . r) by A57, Th7;

then reconsider c2 = c2 as Point of (A . r) by ZFMISC_1:31;

L1 . r is 1 -element by A54, PENCIL_1:12;

then consider c1 being object such that

A58: L1 . r = {c1} by ZFMISC_1:131;

L1 c= Carrier A by PBOOLE:def 18;

then L1 . r c= (Carrier A) . r ;

then {c1} c= [#] (A . r) by A58, Th7;

then reconsider c1 = c1 as Point of (A . r) by ZFMISC_1:31;

A59: now :: thesis: not c1 = c2

c1,c2 are_collinear
by A56, A58, A57;assume A60:
c1 = c2
; :: thesis: contradiction

.= dom L2 by PARTFUN1:def 2 ;

then L1 = L2 by A61;

then B1 /\ B1 = {} by A2, A1, A52;

hence contradiction by A1; :: thesis: verum

end;A61: now :: thesis: for s being object st s in dom L1 holds

L1 . s = L2 . s

dom L1 =
I
by PARTFUN1:def 2
L1 . s = L2 . s

let s be object ; :: thesis: ( s in dom L1 implies L1 . b_{1} = L2 . b_{1} )

assume s in dom L1 ; :: thesis: L1 . b_{1} = L2 . b_{1}

then reconsider s1 = s as Element of I ;

end;assume s in dom L1 ; :: thesis: L1 . b

then reconsider s1 = s as Element of I ;

.= dom L2 by PARTFUN1:def 2 ;

then L1 = L2 by A61;

then B1 /\ B1 = {} by A2, A1, A52;

hence contradiction by A1; :: thesis: verum

then consider bb being Block of (A . r) such that

A62: {c1,c2} c= bb by A59, PENCIL_1:def 1;

let x be Point of (Segre_Product A); :: according to PENCIL_3:def 2 :: thesis: ( x in B1 implies ex y being Point of (Segre_Product A) st

( y in B2 & x,y are_collinear ) )

reconsider x1 = x as Element of Carrier A by Th6;

reconsider y = x1 +* (r,c2) as Point of (Segre_Product A) by PENCIL_1:25;

reconsider y1 = y as ManySortedSet of I ;

assume x in B1 ; :: thesis: ex y being Point of (Segre_Product A) st

( y in B2 & x,y are_collinear )

then A63: ex x2 being Function st

( x2 = x & dom x2 = dom L1 & ( for o being object st o in dom L1 holds

x2 . o in L1 . o ) ) by A1, CARD_3:def 5;

A64: now :: thesis: for a being object st a in dom L2 holds

y1 . a in L2 . a

take
y
; :: thesis: ( y in B2 & x,y are_collinear )y1 . a in L2 . a

let a be object ; :: thesis: ( a in dom L2 implies y1 . b_{1} in L2 . b_{1} )

assume a in dom L2 ; :: thesis: y1 . b_{1} in L2 . b_{1}

then reconsider a1 = a as Element of I ;

end;assume a in dom L2 ; :: thesis: y1 . b

then reconsider a1 = a as Element of I ;

dom y1 = I by PARTFUN1:def 2

.= dom L2 by PARTFUN1:def 2 ;

hence y in B2 by A52, A64, CARD_3:def 5; :: thesis: x,y are_collinear

reconsider B = product ({x1} +* (r,bb)) as Block of (Segre_Product A) by Th16;

A67: now :: thesis: for s being object st s in dom y1 holds

y1 . s in ({x1} +* (r,bb)) . s

dom y1 =
I
by PARTFUN1:def 2
y1 . s in ({x1} +* (r,bb)) . s

let s be object ; :: thesis: ( s in dom y1 implies y1 . b_{1} in ({x1} +* (r,bb)) . b_{1} )

assume s in dom y1 ; :: thesis: y1 . b_{1} in ({x1} +* (r,bb)) . b_{1}

then A68: s in I ;

then A69: ( s in dom {x1} & s in dom x1 ) by PARTFUN1:def 2;

end;assume s in dom y1 ; :: thesis: y1 . b

then A68: s in I ;

then A69: ( s in dom {x1} & s in dom x1 ) by PARTFUN1:def 2;

per cases
( s = r or s <> r )
;

end;

suppose
s = r
; :: thesis: y1 . b_{1} in ({x1} +* (r,bb)) . b_{1}

then
( y1 . s = c2 & bb = ({x1} +* (r,bb)) . s )
by A69, FUNCT_7:31;

hence y1 . s in ({x1} +* (r,bb)) . s by A62, ZFMISC_1:32; :: thesis: verum

end;hence y1 . s in ({x1} +* (r,bb)) . s by A62, ZFMISC_1:32; :: thesis: verum

suppose A70:
s <> r
; :: thesis: y1 . b_{1} in ({x1} +* (r,bb)) . b_{1}

then
{x1} . s = ({x1} +* (r,bb)) . s
by FUNCT_7:32;

then A71: {(x1 . s)} = ({x1} +* (r,bb)) . s by A68, PZFMISC1:def 1;

y1 . s = x1 . s by A70, FUNCT_7:32;

hence y1 . s in ({x1} +* (r,bb)) . s by A71, TARSKI:def 1; :: thesis: verum

end;then A71: {(x1 . s)} = ({x1} +* (r,bb)) . s by A68, PZFMISC1:def 1;

y1 . s = x1 . s by A70, FUNCT_7:32;

hence y1 . s in ({x1} +* (r,bb)) . s by A71, TARSKI:def 1; :: thesis: verum

.= dom ({x1} +* (r,bb)) by PARTFUN1:def 2 ;

then A72: y in B by A67, CARD_3:def 5;

A73: now :: thesis: for s being object st s in dom x1 holds

x1 . s in ({x1} +* (r,bb)) . s

dom x1 =
I
by PARTFUN1:def 2
x1 . s in ({x1} +* (r,bb)) . s

let s be object ; :: thesis: ( s in dom x1 implies x1 . b_{1} in ({x1} +* (r,bb)) . b_{1} )

assume A74: s in dom x1 ; :: thesis: x1 . b_{1} in ({x1} +* (r,bb)) . b_{1}

then A75: s in I ;

then A76: s in dom {x1} by PARTFUN1:def 2;

end;assume A74: s in dom x1 ; :: thesis: x1 . b

then A75: s in I ;

then A76: s in dom {x1} by PARTFUN1:def 2;

per cases
( s = r or s <> r )
;

end;

.= dom ({x1} +* (r,bb)) by PARTFUN1:def 2 ;

then x in B by A73, CARD_3:def 5;

then {x,y} c= B by A72, ZFMISC_1:32;

hence x,y are_collinear by PENCIL_1:def 1; :: thesis: verum