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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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 () 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
defpred S1[ 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 () 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 S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
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 () 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 () 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 ;
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= () . j by A15;
then p in () . 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 ;
A16: c3 . (indx c1) = [#] (A . (indx c1)) by ;
c2 . j is 1 -element by ;
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 ;
product c3 is Subset of () by Th14;
then A19: product c3 is Segre-Coset of A by ;
per cases ( product c1 misses product c3 or product c1 meets product c3 ) ;
suppose A20: product c1 misses product c3 ; :: thesis: ex D being FinSequence of bool the carrier of () 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 ) ) )

diff (c1,c2) = (diff (c1,c3)) + 1 by ;
then consider E being FinSequence of bool the carrier of () 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 ;
then consider F being FinSequence of bool the carrier of () 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;
reconsider D = E ^' F as FinSequence of bool the carrier of () ;
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 ;
then 1 <= len E by FINSEQ_3:25;
hence D . 1 = product c1 by ; :: 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 ;
then 1 <= len F by FINSEQ_3:25;
then A32: len F > 1 by ;
hence D . (len D) = product c2 by ; :: 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
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;
per cases ( D . i in rng E or D . i in rng F ) by ;
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 ; :: thesis: verum
end;
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 ; :: thesis: verum
end;
end;
end;
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 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;
per cases ( i < len E or i >= len E ) ;
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 ;
Di = E . i by ;
hence ( Di misses Di1 & Di '||' Di1 ) by A24, A39, A43, A44; :: thesis: verum
end;
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;
per cases ( k > 0 or k = 0 ) ;
suppose A47: k > 0 ; :: thesis: ( Di misses Di1 & Di '||' Di1 )
((len E) + k) + 1 < (len D) + 1 by ;
then A48: (len E) + (k + 1) < (len E) + (len F) by ;
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 ;
then A51: Di1 = F . ((k + 1) + 1) by ;
0 + 1 <= k by ;
then A52: Di = F . (k + 1) by ;
( 1 <= k + 1 & k + 1 < len F ) by ;
hence ( Di misses Di1 & Di '||' Di1 ) by ; :: thesis: verum
end;
suppose k = 0 ; :: thesis: ( Di misses Di1 & Di '||' Di1 )
then ( Di = F . 1 & Di1 = F . (1 + 1) ) by ;
hence ( Di misses Di1 & Di '||' Di1 ) by ; :: thesis: verum
end;
end;
end;
end;
end;
end;
suppose A53: product c1 meets product c3 ; :: thesis: ex D being FinSequence of bool the carrier of () 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 ) ) )

not p in c2 . j by ;
hence ex D being FinSequence of bool the carrier of () 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;
end;
end;
end;
A54: S1[ 0 ]
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) = 0 implies ex D being FinSequence of bool the carrier of () 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 () 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
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;
dom c1 = I by PARTFUN1:def 2
.= dom c2 by PARTFUN1:def 2 ;
hence ex D being FinSequence of bool the carrier of () 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 ; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A54, A5);
then A58: S1[ diff (b1,b2)] ;
assume indx b1 = indx b2 ; :: thesis: ex D being FinSequence of bool the carrier of () 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 () 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;
given D being FinSequence of bool the carrier of () such that A61: D . 1 = B1 and
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 S1[ Nat] means for bb being non trivial-yielding Segre-like ManySortedSubset of Carrier A st product bb = D . \$1 holds
indx b1 = indx bb;
A65: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A66: S1[k] ; :: thesis: S1[k + 1]
thus S1[k + 1] :: thesis: verum
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 ;
then A69: k + 1 <= len D by FINSEQ_3:25;
per cases ( k = 0 or 0 < k ) ;
suppose k = 0 ; :: thesis: indx b1 = indx bb
hence indx b1 = indx bb by ; :: thesis: verum
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 ;
then k in dom D by ;
then reconsider B0 = D . k as Segre-Coset of A by A63;
reconsider B3 = D . (k + 1) as Segre-Coset of A by ;
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 ;
then A72: ( B0 misses B3 & B0 '||' B3 ) by ;
indx b1 = indx b0 by ;
hence indx b1 = indx bb by ; :: thesis: verum
end;
end;
end;
end;
A73: S1[ 0 ]
proof
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 ; :: thesis: verum
end;
for n being Nat holds S1[n] from hence indx b1 = indx b2 by ; :: thesis: verum