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 B1, B2 being Segre-Coset of A st B1 misses B2 holds

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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 B1, B2 being Segre-Coset of A st B1 misses B2 holds

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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 B1, B2 being Segre-Coset of A st B1 misses B2 holds

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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 Segre-Coset of A; :: thesis: ( B1 misses 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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 A2: B1 misses 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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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: ( B1 = product b1 & B2 = product b2 implies ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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

A3: B1 = product b1 and

A4: B2 = product b2 ; :: thesis: ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) ) )

thus ( indx b1 = indx b2 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) ) ) :: thesis: ( ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) ) implies indx b1 = indx b2 )

A62: D . (len D) = B2 and

A63: for i being Nat st i in dom D holds

D . i is Segre-Coset of A and

A64: 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: indx b1 = indx b2

defpred S_{1}[ Nat] means for bb being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product bb = D . $1 holds

indx b1 = indx bb;

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A73, A65);

hence indx b1 = indx b2 by A4, A62; :: thesis: verum

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

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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 B1, B2 being Segre-Coset of A st B1 misses B2 holds

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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 B1, B2 being Segre-Coset of A st B1 misses B2 holds

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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 Segre-Coset of A; :: thesis: ( B1 misses 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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 A2: B1 misses 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 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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: ( B1 = product b1 & B2 = product b2 implies ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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

A3: B1 = product b1 and

A4: B2 = product b2 ; :: thesis: ( indx b1 = indx b2 iff ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) ) )

thus ( indx b1 = indx b2 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) ) ) :: thesis: ( ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) ) implies indx b1 = indx b2 )

proof

given D being FinSequence of bool the carrier of (Segre_Product A) such that A61:
D . 1 = B1
and
defpred S_{1}[ Nat] means for c1, c2 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st indx c1 = indx c2 & product c1 is Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product c2 & diff (c1,c2) = $1 holds

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

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) );

_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A54, A5);

then A58: S_{1}[ diff (b1,b2)]
;

assume indx b1 = indx b2 ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) )

then consider D being FinSequence of bool the carrier of (Segre_Product A) such that

A59: ( D . 1 = product b1 & D . (len D) = product b2 ) and

A60: ( ( 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 ) ) ) by A2, A3, A4, A58;

take D ; :: thesis: ( D . 1 = B1 & D . (len D) = 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 ) ) )

thus ( D . 1 = B1 & D . (len D) = B2 ) by A3, A4, A59; :: 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 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 ) ) ) by A60; :: thesis: verum

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

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) );

A5: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A54:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A6: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A6: S

thus S

proof

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( indx c1 = indx c2 & product c1 is Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product c2 & diff (c1,c2) = k + 1 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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

A7: indx c1 = indx c2 and

A8: product c1 is Segre-Coset of A and

A9: product c2 is Segre-Coset of A and

product c1 misses product c2 and

A10: diff (c1,c2) = k + 1 ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

{ i where i is Element of I : c1 . i <> c2 . i } <> {} by A10;

then consider j0 being object such that

A11: j0 in { i where i is Element of I : c1 . i <> c2 . i } by XBOOLE_0:def 1;

consider j being Element of I such that

j0 = j and

A12: c1 . j <> c2 . j by A11;

A13: c2 . (indx c1) = [#] (A . (indx c1)) by A7, A9, Th10;

then A14: j <> indx c1 by A8, A12, Th10;

then c1 . j is 1 -element by PENCIL_1:12;

then consider p being object such that

A15: c1 . j = {p} by ZFMISC_1:131;

c1 c= Carrier A by PBOOLE:def 18;

then {p} c= (Carrier A) . j by A15;

then p in (Carrier A) . j by ZFMISC_1:31;

then p in [#] (A . j) by Th7;

then reconsider p = p as Point of (A . j) ;

reconsider c3 = c2 +* (j,{p}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A7, A14, Th13;

A16: c3 . (indx c1) = [#] (A . (indx c1)) by A13, A14, FUNCT_7:32;

c2 . j is 1 -element by A7, A14, PENCIL_1:12;

then A17: ex r being object st c2 . j = {r} by ZFMISC_1:131;

not A . (indx c1) is trivial by Th2;

then A18: indx c3 = indx c1 by A16, PENCIL_1:def 21;

product c3 is Subset of (Segre_Product A) by Th14;

then A19: product c3 is Segre-Coset of A by A16, A18, PENCIL_2:def 2;

end;( D . 1 = product c1 & D . (len D) = product c2 & ( 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

A7: indx c1 = indx c2 and

A8: product c1 is Segre-Coset of A and

A9: product c2 is Segre-Coset of A and

product c1 misses product c2 and

A10: diff (c1,c2) = k + 1 ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

{ i where i is Element of I : c1 . i <> c2 . i } <> {} by A10;

then consider j0 being object such that

A11: j0 in { i where i is Element of I : c1 . i <> c2 . i } by XBOOLE_0:def 1;

consider j being Element of I such that

j0 = j and

A12: c1 . j <> c2 . j by A11;

A13: c2 . (indx c1) = [#] (A . (indx c1)) by A7, A9, Th10;

then A14: j <> indx c1 by A8, A12, Th10;

then c1 . j is 1 -element by PENCIL_1:12;

then consider p being object such that

A15: c1 . j = {p} by ZFMISC_1:131;

c1 c= Carrier A by PBOOLE:def 18;

then {p} c= (Carrier A) . j by A15;

then p in (Carrier A) . j by ZFMISC_1:31;

then p in [#] (A . j) by Th7;

then reconsider p = p as Point of (A . j) ;

reconsider c3 = c2 +* (j,{p}) as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A7, A14, Th13;

A16: c3 . (indx c1) = [#] (A . (indx c1)) by A13, A14, FUNCT_7:32;

c2 . j is 1 -element by A7, A14, PENCIL_1:12;

then A17: ex r being object st c2 . j = {r} by ZFMISC_1:131;

not A . (indx c1) is trivial by Th2;

then A18: indx c3 = indx c1 by A16, PENCIL_1:def 21;

product c3 is Subset of (Segre_Product A) by Th14;

then A19: product c3 is Segre-Coset of A by A16, A18, PENCIL_2:def 2;

per cases
( product c1 misses product c3 or product c1 meets product c3 )
;

end;

suppose A20:
product c1 misses product c3
; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

diff (c1,c2) = (diff (c1,c3)) + 1
by A12, A15, Th19;

then consider E being FinSequence of bool the carrier of (Segre_Product A) such that

A21: E . 1 = product c1 and

A22: E . (len E) = product c3 and

A23: for i being Nat st i in dom E holds

E . i is Segre-Coset of A and

A24: for i being Nat st 1 <= i & i < len E holds

for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds

( Ei misses Ei1 & Ei '||' Ei1 ) by A6, A8, A10, A18, A19, A20;

not p in c2 . j by A12, A15, A17, TARSKI:def 1;

then consider F being FinSequence of bool the carrier of (Segre_Product A) such that

A25: F . 1 = product c3 and

A26: F . (len F) = product c2 and

A27: for i being Nat st i in dom F holds

F . i is Segre-Coset of A and

A28: for i being Nat st 1 <= i & i < len F holds

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

( Di misses Di1 & Di '||' Di1 ) by A1, A9, Th22;

take D ; :: thesis: ( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

1 in dom E by A21, FUNCT_1:def 2;

then 1 <= len E by FINSEQ_3:25;

hence D . 1 = product c1 by A21, FINSEQ_6:140; :: thesis: ( D . (len D) = product c2 & ( 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 ) ) )

A31: 1 in dom F by A25, FUNCT_1:def 2;

then 1 <= len F by FINSEQ_3:25;

then A32: len F > 1 by A29, XXREAL_0:1;

hence D . (len D) = product c2 by A26, FINSEQ_6:142; :: 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 i being Nat st i in dom D holds

D . i 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 )

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

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

end;then consider E being FinSequence of bool the carrier of (Segre_Product A) such that

A21: E . 1 = product c1 and

A22: E . (len E) = product c3 and

A23: for i being Nat st i in dom E holds

E . i is Segre-Coset of A and

A24: for i being Nat st 1 <= i & i < len E holds

for Ei, Ei1 being Segre-Coset of A st Ei = E . i & Ei1 = E . (i + 1) holds

( Ei misses Ei1 & Ei '||' Ei1 ) by A6, A8, A10, A18, A19, A20;

not p in c2 . j by A12, A15, A17, TARSKI:def 1;

then consider F being FinSequence of bool the carrier of (Segre_Product A) such that

A25: F . 1 = product c3 and

A26: F . (len F) = product c2 and

A27: for i being Nat st i in dom F holds

F . i is Segre-Coset of A and

A28: for i being Nat st 1 <= i & i < len F holds

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

( Di misses Di1 & Di '||' Di1 ) by A1, A9, Th22;

A29: now :: thesis: not len F = 1

reconsider D = E ^' F as FinSequence of bool the carrier of (Segre_Product A) ;
dom c2 = I
by PARTFUN1:def 2;

then A30: c3 . j = {p} by FUNCT_7:31;

assume len F = 1 ; :: thesis: contradiction

hence contradiction by A12, A15, A25, A26, A30, PUA2MSS1:2; :: thesis: verum

end;then A30: c3 . j = {p} by FUNCT_7:31;

assume len F = 1 ; :: thesis: contradiction

hence contradiction by A12, A15, A25, A26, A30, PUA2MSS1:2; :: thesis: verum

take D ; :: thesis: ( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

1 in dom E by A21, FUNCT_1:def 2;

then 1 <= len E by FINSEQ_3:25;

hence D . 1 = product c1 by A21, FINSEQ_6:140; :: thesis: ( D . (len D) = product c2 & ( 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 ) ) )

A31: 1 in dom F by A25, FUNCT_1:def 2;

then 1 <= len F by FINSEQ_3:25;

then A32: len F > 1 by A29, XXREAL_0:1;

hence D . (len D) = product c2 by A26, FINSEQ_6:142; :: 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 i being Nat st i in dom D holds

D . i 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

thus
for i being Nat st 1 <= i & i < len D holds
let i be Nat; :: thesis: ( i in dom D implies D . i is Segre-Coset of A )

A33: rng D c= (rng E) \/ (rng F) by FINSEQ_6:143;

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

then A34: D . i in rng D by FUNCT_1:3;

end;A33: rng D c= (rng E) \/ (rng F) by FINSEQ_6:143;

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

then A34: D . i in rng D by FUNCT_1:3;

per cases
( D . i in rng E or D . i in rng F )
by A34, A33, XBOOLE_0:def 3;

end;

suppose
D . i in rng E
; :: thesis: D . i is Segre-Coset of A

then consider i0 being object such that

A35: i0 in dom E and

A36: D . i = E . i0 by FUNCT_1:def 3;

thus D . i is Segre-Coset of A by A23, A35, A36; :: thesis: verum

end;A35: i0 in dom E and

A36: D . i = E . i0 by FUNCT_1:def 3;

thus D . i is Segre-Coset of A by A23, A35, A36; :: thesis: verum

suppose
D . i in rng F
; :: thesis: D . i is Segre-Coset of A

then consider i0 being object such that

A37: i0 in dom F and

A38: D . i = F . i0 by FUNCT_1:def 3;

thus D . i is Segre-Coset of A by A27, A37, A38; :: thesis: verum

end;A37: i0 in dom F and

A38: D . i = F . i0 by FUNCT_1:def 3;

thus D . i is Segre-Coset of A by A27, A37, A38; :: thesis: verum

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 i be Nat; :: thesis: ( 1 <= i & i < len D implies for Di, Di1 being Segre-Coset of A st Di = D . i & Di1 = D . (i + 1) holds

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

assume that

A39: 1 <= i and

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

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

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

assume that

A41: Di = D . i and

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

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

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

assume that

A39: 1 <= i and

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

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

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

assume that

A41: Di = D . i and

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

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

per cases
( i < len E or i >= len E )
;

end;

suppose A43:
i < len E
; :: thesis: ( Di misses Di1 & Di '||' Di1 )

then
i + 1 <= len E
by NAT_1:13;

then A44: Di1 = E . (i + 1) by A42, FINSEQ_6:140, NAT_1:11;

Di = E . i by A39, A41, A43, FINSEQ_6:140;

hence ( Di misses Di1 & Di '||' Di1 ) by A24, A39, A43, A44; :: thesis: verum

end;then A44: Di1 = E . (i + 1) by A42, FINSEQ_6:140, NAT_1:11;

Di = E . i by A39, A41, A43, FINSEQ_6:140;

hence ( Di misses Di1 & Di '||' Di1 ) by A24, A39, A43, A44; :: thesis: verum

suppose
i >= len E
; :: thesis: ( Di misses Di1 & Di '||' Di1 )

then consider k being Nat such that

A45: i = (len E) + k by NAT_1:10;

A46: F <> {} by A31;

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

end;A45: i = (len E) + k by NAT_1:10;

A46: F <> {} by A31;

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

per cases
( k > 0 or k = 0 )
;

end;

suppose A47:
k > 0
; :: thesis: ( Di misses Di1 & Di '||' Di1 )

((len E) + k) + 1 < (len D) + 1
by A40, A45, XREAL_1:6;

then A48: (len E) + (k + 1) < (len E) + (len F) by A46, FINSEQ_6:139;

then A49: k + 1 < len F by XREAL_1:6;

then A50: k < len F by NAT_1:13;

Di1 = D . ((len E) + (k + 1)) by A42, A45;

then A51: Di1 = F . ((k + 1) + 1) by A49, FINSEQ_6:141, NAT_1:11;

0 + 1 <= k by A47, NAT_1:13;

then A52: Di = F . (k + 1) by A41, A45, A50, FINSEQ_6:141;

( 1 <= k + 1 & k + 1 < len F ) by A48, NAT_1:11, XREAL_1:6;

hence ( Di misses Di1 & Di '||' Di1 ) by A28, A52, A51; :: thesis: verum

end;then A48: (len E) + (k + 1) < (len E) + (len F) by A46, FINSEQ_6:139;

then A49: k + 1 < len F by XREAL_1:6;

then A50: k < len F by NAT_1:13;

Di1 = D . ((len E) + (k + 1)) by A42, A45;

then A51: Di1 = F . ((k + 1) + 1) by A49, FINSEQ_6:141, NAT_1:11;

0 + 1 <= k by A47, NAT_1:13;

then A52: Di = F . (k + 1) by A41, A45, A50, FINSEQ_6:141;

( 1 <= k + 1 & k + 1 < len F ) by A48, NAT_1:11, XREAL_1:6;

hence ( Di misses Di1 & Di '||' Di1 ) by A28, A52, A51; :: thesis: verum

suppose A53:
product c1 meets product c3
; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

not p in c2 . j
by A12, A15, A17, TARSKI:def 1;

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

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) ) by A1, A8, A9, A18, A19, A53, Th11, Th22; :: thesis: verum

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

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) ) by A1, A8, A9, A18, A19, A53, Th11, Th22; :: thesis: verum

proof

for n being Nat holds S
let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( indx c1 = indx c2 & product c1 is Segre-Coset of A & product c2 is Segre-Coset of A & product c1 misses product c2 & diff (c1,c2) = 0 implies ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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

indx c1 = indx c2 and

product c1 is Segre-Coset of A and

product c2 is Segre-Coset of A and

A55: product c1 misses product c2 and

A56: diff (c1,c2) = 0 ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

.= dom c2 by PARTFUN1:def 2 ;

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

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) ) by A55, A57, FUNCT_1:2; :: thesis: verum

end;( D . 1 = product c1 & D . (len D) = product c2 & ( 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

indx c1 = indx c2 and

product c1 is Segre-Coset of A and

product c2 is Segre-Coset of A and

A55: product c1 misses product c2 and

A56: diff (c1,c2) = 0 ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) )

A57: now :: thesis: for a being object st a in dom c1 holds

not c1 . a <> c2 . a

dom c1 =
I
by PARTFUN1:def 2
not c1 . a <> c2 . a

let a be object ; :: thesis: ( a in dom c1 implies not c1 . a <> c2 . a )

assume a in dom c1 ; :: thesis: not c1 . a <> c2 . a

then reconsider j = a as Element of I ;

assume c1 . a <> c2 . a ; :: thesis: contradiction

then j in { i where i is Element of I : c1 . i <> c2 . i } ;

hence contradiction by A56; :: thesis: verum

end;assume a in dom c1 ; :: thesis: not c1 . a <> c2 . a

then reconsider j = a as Element of I ;

assume c1 . a <> c2 . a ; :: thesis: contradiction

then j in { i where i is Element of I : c1 . i <> c2 . i } ;

hence contradiction by A56; :: thesis: verum

.= dom c2 by PARTFUN1:def 2 ;

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

( D . 1 = product c1 & D . (len D) = product c2 & ( 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 ) ) ) by A55, A57, FUNCT_1:2; :: thesis: verum

then A58: S

assume indx b1 = indx b2 ; :: thesis: ex D being FinSequence of bool the carrier of (Segre_Product A) st

( D . 1 = B1 & D . (len D) = 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 ) ) )

then consider D being FinSequence of bool the carrier of (Segre_Product A) such that

A59: ( D . 1 = product b1 & D . (len D) = product b2 ) and

A60: ( ( 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 ) ) ) by A2, A3, A4, A58;

take D ; :: thesis: ( D . 1 = B1 & D . (len D) = 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 ) ) )

thus ( D . 1 = B1 & D . (len D) = B2 ) by A3, A4, A59; :: 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 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 ) ) ) by A60; :: thesis: verum

A62: D . (len D) = B2 and

A63: for i being Nat st i in dom D holds

D . i is Segre-Coset of A and

A64: 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: indx b1 = indx b2

defpred S

indx b1 = indx bb;

A65: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

A73:
SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A66: S_{1}[k]
; :: thesis: S_{1}[k + 1]

thus S_{1}[k + 1]
:: thesis: verum

end;assume A66: S

thus S

proof

let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product bb = D . (k + 1) implies indx b1 = indx bb )

assume A67: product bb = D . (k + 1) ; :: thesis: indx b1 = indx bb

A68: k + 1 in dom D by A67, FUNCT_1:def 2;

then A69: k + 1 <= len D by FINSEQ_3:25;

end;assume A67: product bb = D . (k + 1) ; :: thesis: indx b1 = indx bb

A68: k + 1 in dom D by A67, FUNCT_1:def 2;

then A69: k + 1 <= len D by FINSEQ_3:25;

per cases
( k = 0 or 0 < k )
;

end;

suppose
0 < k
; :: thesis: indx b1 = indx bb

then
0 + 1 < k + 1
by XREAL_1:6;

then A70: 1 <= k by NAT_1:13;

k <= len D by A69, NAT_1:13;

then k in dom D by A70, FINSEQ_3:25;

then reconsider B0 = D . k as Segre-Coset of A by A63;

reconsider B3 = D . (k + 1) as Segre-Coset of A by A63, A68;

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

A71: B0 = product b0 and

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

k < len D by A69, NAT_1:13;

then A72: ( B0 misses B3 & B0 '||' B3 ) by A64, A70;

indx b1 = indx b0 by A66, A71;

hence indx b1 = indx bb by A67, A71, A72, Th21; :: thesis: verum

end;then A70: 1 <= k by NAT_1:13;

k <= len D by A69, NAT_1:13;

then k in dom D by A70, FINSEQ_3:25;

then reconsider B0 = D . k as Segre-Coset of A by A63;

reconsider B3 = D . (k + 1) as Segre-Coset of A by A63, A68;

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

A71: B0 = product b0 and

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

k < len D by A69, NAT_1:13;

then A72: ( B0 misses B3 & B0 '||' B3 ) by A64, A70;

indx b1 = indx b0 by A66, A71;

hence indx b1 = indx bb by A67, A71, A72, Th21; :: thesis: verum

proof

for n being Nat holds S
A74:
not 0 in dom D
by FINSEQ_3:24;

let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product bb = D . 0 implies indx b1 = indx bb )

assume product bb = D . 0 ; :: thesis: indx b1 = indx bb

hence indx b1 = indx bb by A74, FUNCT_1:def 2; :: thesis: verum

end;let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( product bb = D . 0 implies indx b1 = indx bb )

assume product bb = D . 0 ; :: thesis: indx b1 = indx bb

hence indx b1 = indx bb by A74, FUNCT_1:def 2; :: thesis: verum

hence indx b1 = indx b2 by A4, A62; :: thesis: verum