let I be non empty finite set ; :: thesis: for A being PLS-yielding ManySortedSet of I st ( for i being Element of I holds A . i is connected ) holds

for i being Element of I

for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is connected ) implies for i being Element of I

for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) ) )

assume A1: for i being Element of I holds A . i is connected ; :: thesis: for i being Element of I

for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let i be Element of I; :: thesis: for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let p be Point of (A . i); :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i implies ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) ) )

assume that

A2: product b2 is Segre-Coset of A and

A3: b1 = b2 +* (i,{p}) and

A4: not p in b2 . i ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

defpred S_{1}[ set , set ] means for a, b being Point of (A . i) st $1 = a & $2 = b holds

a,b are_collinear ;

then consider q being object such that

A6: b2 . i = {q} by ZFMISC_1:131;

b2 c= Carrier A by PBOOLE:def 18;

then b2 . i c= (Carrier A) . i ;

then {q} c= [#] (A . i) by A6, Th7;

then reconsider q = q as Point of (A . i) by ZFMISC_1:31;

A . i is connected by A1;

then consider f being FinSequence of the carrier of (A . i) such that

A7: ( p = f . 1 & q = f . (len f) ) and

A8: for j being Nat st 1 <= j & j < len f holds

for a, b being Point of (A . i) st a = f . j & b = f . (j + 1) holds

a,b are_collinear by PENCIL_1:def 10;

A9: for j being Element of NAT

for x, y being set st 1 <= j & j < len f & x = f . j & y = f . (j + 1) holds

S_{1}[x,y]
by A8;

consider F being one-to-one FinSequence of the carrier of (A . i) such that

A10: ( p = F . 1 & q = F . (len F) & rng F c= rng f & ( for j being Element of NAT st 1 <= j & j < len F holds

S_{1}[F . j,F . (j + 1)] ) )
from PENCIL_2:sch 1(A7, A9);

_{1}( set ) -> set = product (b2 +* (i,{(F . $1)}));

consider G being FinSequence such that

A12: ( len G = len F & ( for j being Nat st j in dom G holds

G . j = H_{1}(j) ) )
from FINSEQ_1:sch 2();

rng G c= bool the carrier of (Segre_Product A)

take D ; :: thesis: ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

A16: dom G = Seg (len F) by A12, FINSEQ_1:def 3;

dom F = Seg (len F) by FINSEQ_1:def 3;

hence D . 1 = product b1 by A3, A10, A12, A16, A11, FINSEQ_3:32; :: thesis: ( D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

D . (len D) = product (b2 +* (i,{(F . (len F))})) by A12, A16, A11, FINSEQ_1:3;

hence D . (len D) = product b2 by A6, A10, FUNCT_7:35; :: thesis: ( ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

thus for j being Nat st j in dom D holds

D . j is Segre-Coset of A :: thesis: for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 )

thus for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) :: thesis: verum

for i being Element of I

for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: ( ( for i being Element of I holds A . i is connected ) implies for i being Element of I

for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) ) )

assume A1: for i being Element of I holds A . i is connected ; :: thesis: for i being Element of I

for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let i be Element of I; :: thesis: for p being Point of (A . i)

for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let p be Point of (A . i); :: thesis: for b1, b2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i holds

ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product b2 is Segre-Coset of A & b1 = b2 +* (i,{p}) & not p in b2 . i implies ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) ) )

assume that

A2: product b2 is Segre-Coset of A and

A3: b1 = b2 +* (i,{p}) and

A4: not p in b2 . i ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

defpred S

a,b are_collinear ;

A5: now :: thesis: not i = indx b2

then
b2 . i is 1 -element
by PENCIL_1:12;assume
i = indx b2
; :: thesis: contradiction

then b2 . i = [#] (A . i) by A2, Th10;

hence contradiction by A4; :: thesis: verum

end;then b2 . i = [#] (A . i) by A2, Th10;

hence contradiction by A4; :: thesis: verum

then consider q being object such that

A6: b2 . i = {q} by ZFMISC_1:131;

b2 c= Carrier A by PBOOLE:def 18;

then b2 . i c= (Carrier A) . i ;

then {q} c= [#] (A . i) by A6, Th7;

then reconsider q = q as Point of (A . i) by ZFMISC_1:31;

A . i is connected by A1;

then consider f being FinSequence of the carrier of (A . i) such that

A7: ( p = f . 1 & q = f . (len f) ) and

A8: for j being Nat st 1 <= j & j < len f holds

for a, b being Point of (A . i) st a = f . j & b = f . (j + 1) holds

a,b are_collinear by PENCIL_1:def 10;

A9: for j being Element of NAT

for x, y being set st 1 <= j & j < len f & x = f . j & y = f . (j + 1) holds

S

consider F being one-to-one FinSequence of the carrier of (A . i) such that

A10: ( p = F . 1 & q = F . (len F) & rng F c= rng f & ( for j being Element of NAT st 1 <= j & j < len F holds

S

A11: now :: thesis: not F = {}

deffunc Hassume
F = {}
; :: thesis: contradiction

then dom F = {} ;

then ( F . 1 = {} & F . (len F) = {} ) by FUNCT_1:def 2;

hence contradiction by A4, A6, A10, TARSKI:def 1; :: thesis: verum

end;then dom F = {} ;

then ( F . 1 = {} & F . (len F) = {} ) by FUNCT_1:def 2;

hence contradiction by A4, A6, A10, TARSKI:def 1; :: thesis: verum

consider G being FinSequence such that

A12: ( len G = len F & ( for j being Nat st j in dom G holds

G . j = H

rng G c= bool the carrier of (Segre_Product A)

proof

then reconsider D = G as FinSequence of bool the carrier of (Segre_Product A) by FINSEQ_1:def 4;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng G or a in bool the carrier of (Segre_Product A) )

assume a in rng G ; :: thesis: a in bool the carrier of (Segre_Product A)

then consider o being object such that

A13: o in dom G and

A14: G . o = a by FUNCT_1:def 3;

reconsider o = o as Element of NAT by A13;

dom G = dom F by A12, FINSEQ_3:29;

then F . o in rng F by A13, FUNCT_1:3;

then {(F . o)} is Subset of (A . i) by ZFMISC_1:31;

then A15: product (b2 +* (i,{(F . o)})) is Subset of (Segre_Product A) by Th14;

G . o = product (b2 +* (i,{(F . o)})) by A12, A13;

hence a in bool the carrier of (Segre_Product A) by A14, A15; :: thesis: verum

end;assume a in rng G ; :: thesis: a in bool the carrier of (Segre_Product A)

then consider o being object such that

A13: o in dom G and

A14: G . o = a by FUNCT_1:def 3;

reconsider o = o as Element of NAT by A13;

dom G = dom F by A12, FINSEQ_3:29;

then F . o in rng F by A13, FUNCT_1:3;

then {(F . o)} is Subset of (A . i) by ZFMISC_1:31;

then A15: product (b2 +* (i,{(F . o)})) is Subset of (Segre_Product A) by Th14;

G . o = product (b2 +* (i,{(F . o)})) by A12, A13;

hence a in bool the carrier of (Segre_Product A) by A14, A15; :: thesis: verum

take D ; :: thesis: ( D . 1 = product b1 & D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

A16: dom G = Seg (len F) by A12, FINSEQ_1:def 3;

dom F = Seg (len F) by FINSEQ_1:def 3;

hence D . 1 = product b1 by A3, A10, A12, A16, A11, FINSEQ_3:32; :: thesis: ( D . (len D) = product b2 & ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

D . (len D) = product (b2 +* (i,{(F . (len F))})) by A12, A16, A11, FINSEQ_1:3;

hence D . (len D) = product b2 by A6, A10, FUNCT_7:35; :: thesis: ( ( for i being Nat st i in dom D holds

D . i is Segre-Coset of A ) & ( for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) ) )

thus for j being Nat st j in dom D holds

D . j is Segre-Coset of A :: thesis: for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 )

proof

A21:
dom b2 = I
by PARTFUN1:def 2;
let j be Nat; :: thesis: ( j in dom D implies D . j is Segre-Coset of A )

assume A17: j in dom D ; :: thesis: D . j is Segre-Coset of A

then j in Seg (len F) by A12, FINSEQ_1:def 3;

then j in dom F by FINSEQ_1:def 3;

then F . j in rng F by FUNCT_1:3;

then reconsider Fj = F . j as Point of (A . i) ;

reconsider BB = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;

BB . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;

then not BB . (indx b2) is trivial by PENCIL_1:def 21;

then A18: indx BB = indx b2 by PENCIL_1:def 21;

then A19: BB . (indx BB) = b2 . (indx b2) by A5, FUNCT_7:32

.= [#] (A . (indx BB)) by A2, A18, Th10 ;

A20: D . j = product BB by A12, A17;

then D . j is Subset of (Segre_Product A) by Th14;

hence D . j is Segre-Coset of A by A20, A19, PENCIL_2:def 2; :: thesis: verum

end;assume A17: j in dom D ; :: thesis: D . j is Segre-Coset of A

then j in Seg (len F) by A12, FINSEQ_1:def 3;

then j in dom F by FINSEQ_1:def 3;

then F . j in rng F by FUNCT_1:3;

then reconsider Fj = F . j as Point of (A . i) ;

reconsider BB = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;

BB . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;

then not BB . (indx b2) is trivial by PENCIL_1:def 21;

then A18: indx BB = indx b2 by PENCIL_1:def 21;

then A19: BB . (indx BB) = b2 . (indx b2) by A5, FUNCT_7:32

.= [#] (A . (indx BB)) by A2, A18, Th10 ;

A20: D . j = product BB by A12, A17;

then D . j is Subset of (Segre_Product A) by Th14;

hence D . j is Segre-Coset of A by A20, A19, PENCIL_2:def 2; :: thesis: verum

thus for i being Nat st 1 <= i & i < len D holds

for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

( Di misses Di1 & Di '||' Di1 ) :: thesis: verum

proof

let j be Nat; :: thesis: ( 1 <= j & j < len D implies for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds

( Di misses Di1 & Di '||' Di1 ) )

assume A22: ( 1 <= j & j < len D ) ; :: thesis: for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds

( Di misses Di1 & Di '||' Di1 )

let Di, Di1 be Segre-Coset of A; :: thesis: ( Di = D . j & Di1 = D . (j + 1) implies ( Di misses Di1 & Di '||' Di1 ) )

assume that

A23: Di = D . j and

A24: Di1 = D . (j + 1) ; :: thesis: ( Di misses Di1 & Di '||' Di1 )

reconsider j = j as Element of NAT by ORDINAL1:def 12;

j in dom D by A22, FINSEQ_3:25;

then j in Seg (len F) by A12, FINSEQ_1:def 3;

then j in dom F by FINSEQ_1:def 3;

then F . j in rng F by FUNCT_1:3;

then reconsider Fj = F . j as Point of (A . i) ;

reconsider BB1 = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;

A25: j in dom D by A22, FINSEQ_3:25;

then A26: D . j = product BB1 by A12;

( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13;

then j + 1 in dom D by FINSEQ_3:25;

then j + 1 in Seg (len F) by A12, FINSEQ_1:def 3;

then j + 1 in dom F by FINSEQ_1:def 3;

then F . (j + 1) in rng F by FUNCT_1:3;

then reconsider Fj2 = F . (j + 1) as Point of (A . i) ;

reconsider BB2 = b2 +* (i,{Fj2}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;

( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13;

then A27: j + 1 in dom D by FINSEQ_3:25;

then A28: j + 1 in Seg (len F) by A12, FINSEQ_1:def 3;

A29: D . (j + 1) = product BB2 by A12, A27;

A30: j in Seg (len F) by A12, A25, FINSEQ_1:def 3;

thus A31: Di misses Di1 :: thesis: Di '||' Di1

end;( Di misses Di1 & Di '||' Di1 ) )

assume A22: ( 1 <= j & j < len D ) ; :: thesis: for Di, Di1 being Segre-Coset of A st Di = D . j & Di1 = D . (j + 1) holds

( Di misses Di1 & Di '||' Di1 )

let Di, Di1 be Segre-Coset of A; :: thesis: ( Di = D . j & Di1 = D . (j + 1) implies ( Di misses Di1 & Di '||' Di1 ) )

assume that

A23: Di = D . j and

A24: Di1 = D . (j + 1) ; :: thesis: ( Di misses Di1 & Di '||' Di1 )

reconsider j = j as Element of NAT by ORDINAL1:def 12;

j in dom D by A22, FINSEQ_3:25;

then j in Seg (len F) by A12, FINSEQ_1:def 3;

then j in dom F by FINSEQ_1:def 3;

then F . j in rng F by FUNCT_1:3;

then reconsider Fj = F . j as Point of (A . i) ;

reconsider BB1 = b2 +* (i,{Fj}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;

A25: j in dom D by A22, FINSEQ_3:25;

then A26: D . j = product BB1 by A12;

( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13;

then j + 1 in dom D by FINSEQ_3:25;

then j + 1 in Seg (len F) by A12, FINSEQ_1:def 3;

then j + 1 in dom F by FINSEQ_1:def 3;

then F . (j + 1) in rng F by FUNCT_1:3;

then reconsider Fj2 = F . (j + 1) as Point of (A . i) ;

reconsider BB2 = b2 +* (i,{Fj2}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A5, Th13;

( 1 <= j + 1 & j + 1 <= len D ) by A22, NAT_1:13;

then A27: j + 1 in dom D by FINSEQ_3:25;

then A28: j + 1 in Seg (len F) by A12, FINSEQ_1:def 3;

A29: D . (j + 1) = product BB2 by A12, A27;

A30: j in Seg (len F) by A12, A25, FINSEQ_1:def 3;

thus A31: Di misses Di1 :: thesis: Di '||' Di1

proof

A32:
j <> j + 1
;

assume Di /\ Di1 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A33: x in Di /\ Di1 by XBOOLE_0:def 1;

x in Di1 by A33, XBOOLE_0:def 4;

then consider x2 being Function such that

A34: x2 = x and

dom x2 = dom (b2 +* (i,{(F . (j + 1))})) and

A35: for o being object st o in dom (b2 +* (i,{(F . (j + 1))})) holds

x2 . o in (b2 +* (i,{(F . (j + 1))})) . o by A24, A29, CARD_3:def 5;

dom (b2 +* (i,{(F . (j + 1))})) = I by PARTFUN1:def 2;

then x2 . i in (b2 +* (i,{(F . (j + 1))})) . i by A35;

then x2 . i in {(F . (j + 1))} by A21, FUNCT_7:31;

then A36: x2 . i = F . (j + 1) by TARSKI:def 1;

x in Di by A33, XBOOLE_0:def 4;

then consider x1 being Function such that

A37: x1 = x and

dom x1 = dom (b2 +* (i,{(F . j)})) and

A38: for o being object st o in dom (b2 +* (i,{(F . j)})) holds

x1 . o in (b2 +* (i,{(F . j)})) . o by A23, A26, CARD_3:def 5;

dom (b2 +* (i,{(F . j)})) = I by PARTFUN1:def 2;

then x1 . i in (b2 +* (i,{(F . j)})) . i by A38;

then x1 . i in {(F . j)} by A21, FUNCT_7:31;

then A39: x1 . i = F . j by TARSKI:def 1;

( j in dom F & j + 1 in dom F ) by A30, A28, FINSEQ_1:def 3;

hence contradiction by A37, A34, A39, A36, A32, FUNCT_1:def 4; :: thesis: verum

end;assume Di /\ Di1 <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A33: x in Di /\ Di1 by XBOOLE_0:def 1;

x in Di1 by A33, XBOOLE_0:def 4;

then consider x2 being Function such that

A34: x2 = x and

dom x2 = dom (b2 +* (i,{(F . (j + 1))})) and

A35: for o being object st o in dom (b2 +* (i,{(F . (j + 1))})) holds

x2 . o in (b2 +* (i,{(F . (j + 1))})) . o by A24, A29, CARD_3:def 5;

dom (b2 +* (i,{(F . (j + 1))})) = I by PARTFUN1:def 2;

then x2 . i in (b2 +* (i,{(F . (j + 1))})) . i by A35;

then x2 . i in {(F . (j + 1))} by A21, FUNCT_7:31;

then A36: x2 . i = F . (j + 1) by TARSKI:def 1;

x in Di by A33, XBOOLE_0:def 4;

then consider x1 being Function such that

A37: x1 = x and

dom x1 = dom (b2 +* (i,{(F . j)})) and

A38: for o being object st o in dom (b2 +* (i,{(F . j)})) holds

x1 . o in (b2 +* (i,{(F . j)})) . o by A23, A26, CARD_3:def 5;

dom (b2 +* (i,{(F . j)})) = I by PARTFUN1:def 2;

then x1 . i in (b2 +* (i,{(F . j)})) . i by A38;

then x1 . i in {(F . j)} by A21, FUNCT_7:31;

then A39: x1 . i = F . j by TARSKI:def 1;

( j in dom F & j + 1 in dom F ) by A30, A28, FINSEQ_1:def 3;

hence contradiction by A37, A34, A39, A36, A32, FUNCT_1:def 4; :: thesis: verum

now :: thesis: for c1, c2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st Di = product c1 & Di1 = product c2 holds

( indx c1 = indx c2 & ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) ) )

hence
Di '||' Di1
by A31, Th21; :: thesis: verum( indx c1 = indx c2 & ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) ) )

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( Di = product c1 & Di1 = product c2 implies ( indx c1 = indx c2 & ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) ) ) )

assume that

A40: Di = product c1 and

A41: Di1 = product c2 ; :: thesis: ( indx c1 = indx c2 & ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) ) )

A42: c2 = b2 +* (i,{(F . (j + 1))}) by A24, A29, A41, PUA2MSS1:2;

then c2 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;

then A43: not c2 . (indx b2) is trivial by PENCIL_1:def 21;

A44: c1 = b2 +* (i,{(F . j)}) by A23, A26, A40, PUA2MSS1:2;

then c1 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;

then A45: not c1 . (indx b2) is trivial by PENCIL_1:def 21;

then indx c1 = indx b2 by PENCIL_1:def 21;

hence indx c1 = indx c2 by A43, PENCIL_1:def 21; :: thesis: ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) )

take r = i; :: thesis: ( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) )

thus r <> indx c1 by A5, A45, PENCIL_1:def 21; :: thesis: ( ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) )

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

c1 . j = c2 . j :: thesis: for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear

p1,p2 are_collinear :: thesis: verum

end;( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) ) ) )

assume that

A40: Di = product c1 and

A41: Di1 = product c2 ; :: thesis: ( indx c1 = indx c2 & ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) ) )

A42: c2 = b2 +* (i,{(F . (j + 1))}) by A24, A29, A41, PUA2MSS1:2;

then c2 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;

then A43: not c2 . (indx b2) is trivial by PENCIL_1:def 21;

A44: c1 = b2 +* (i,{(F . j)}) by A23, A26, A40, PUA2MSS1:2;

then c1 . (indx b2) = b2 . (indx b2) by A5, FUNCT_7:32;

then A45: not c1 . (indx b2) is trivial by PENCIL_1:def 21;

then indx c1 = indx b2 by PENCIL_1:def 21;

hence indx c1 = indx c2 by A43, PENCIL_1:def 21; :: thesis: ex r being Element of I st

( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) )

take r = i; :: thesis: ( r <> indx c1 & ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) )

thus r <> indx c1 by A5, A45, PENCIL_1:def 21; :: thesis: ( ( for j being Element of I st j <> r holds

c1 . j = c2 . j ) & ( for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear ) )

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

c1 . j = c2 . j :: thesis: for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds

p1,p2 are_collinear

proof

thus
for p1, p2 being Point of (A . r) st c1 . r = {p1} & c2 . r = {p2} holds
let j be Element of I; :: thesis: ( j <> r implies c1 . j = c2 . j )

assume A46: j <> r ; :: thesis: c1 . j = c2 . j

hence c1 . j = b2 . j by A44, FUNCT_7:32

.= c2 . j by A42, A46, FUNCT_7:32 ;

:: thesis: verum

end;assume A46: j <> r ; :: thesis: c1 . j = c2 . j

hence c1 . j = b2 . j by A44, FUNCT_7:32

.= c2 . j by A42, A46, FUNCT_7:32 ;

:: thesis: verum

p1,p2 are_collinear :: thesis: verum

proof

let p1, p2 be Point of (A . r); :: thesis: ( c1 . r = {p1} & c2 . r = {p2} implies p1,p2 are_collinear )

assume that

A47: c1 . r = {p1} and

A48: c2 . r = {p2} ; :: thesis: p1,p2 are_collinear

c2 . r = {(F . (j + 1))} by A21, A42, FUNCT_7:31;

then A49: F . (j + 1) = p2 by A48, ZFMISC_1:3;

c1 . r = {(F . j)} by A21, A44, FUNCT_7:31;

then F . j = p1 by A47, ZFMISC_1:3;

hence p1,p2 are_collinear by A10, A12, A22, A49; :: thesis: verum

end;assume that

A47: c1 . r = {p1} and

A48: c2 . r = {p2} ; :: thesis: p1,p2 are_collinear

c2 . r = {(F . (j + 1))} by A21, A42, FUNCT_7:31;

then A49: F . (j + 1) = p2 by A48, ZFMISC_1:3;

c1 . r = {(F . j)} by A21, A44, FUNCT_7:31;

then F . j = p1 by A47, ZFMISC_1:3;

hence p1,p2 are_collinear by A10, A12, A22, A49; :: thesis: verum