let I be non empty finite set ; :: thesis:
let A be PLS-yielding ManySortedSet of I; :: thesis:
assume A1: for i being Element of I holds A . i is connected ; :: thesis:
let B1, B2 be Segre-Coset of A; :: thesis:
assume A2: B1 misses B2 ; :: thesis:
let b1, b2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume that
A3: B1 = product b1 and
A4: B2 = product b2 ; :: thesis:
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:

proof

defpred S₁[ 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 ) ) );

A5: now :: thesis:

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
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:
{ 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 ;

suppose A20: product c1 misses product c3 ; :: thesis:

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;

A29: now :: thesis:

dom c2 = I by PARTFUN1:def 2;
then A30: c3 . j = {p} by FUNCT_7:31;
assume len F = 1 ; :: thesis:
hence contradiction by A12, A15, A25, A26, A30, PUA2MSS1:2; :: thesis:

end;

reconsider D = E ^' F as FinSequence of bool the carrier of (Segre_Product A) ;
take D ; :: thesis:
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:
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:
thus for i being Nat st i in dom D holds
D . i is Segre-Coset of A :: thesis:

proof

let i be Nat; :: thesis:
A33: rng D c= (rng E) \/ (rng F) by FINSEQ_6:143;
assume i in dom D ; :: thesis:
then A34: D . i in rng D by FUNCT_1:3;

per cases by A34, A33, XBOOLE_0:def 3;

suppose D . i in rng E ; :: thesis:

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:

end;

suppose D . i in rng F ; :: thesis:

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:

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:

proof

let i be Nat; :: thesis:
assume that
A39: 1 <= i and
A40: i < len D ; :: thesis:
let Di, Di1 be Segre-Coset of A; :: thesis:
assume that
A41: Di = D . i and
A42: Di1 = D . (i + 1) ; :: thesis:
reconsider i = i as Element of NAT by ORDINAL1:def 12;

per cases ;

suppose A43: i < len E ; :: thesis:

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:

end;

suppose i >= len E ; :: thesis:

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 ;

suppose A47: k > 0 ; :: thesis:

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

end;

suppose k = 0 ; :: thesis:

then ( Di = F . 1 & Di1 = F . (1 + 1) ) by A22, A25, A32, A39, A41, A42, A45, FINSEQ_6:140, FINSEQ_6:141;
hence ( Di misses Di1 & Di '||' Di1 ) by A28, A32; :: thesis:

end;

suppose A53: product c1 meets product c3 ; :: thesis:

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:

end;

A54: S₁[ 0 ]

proof

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
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:

A57: now :: thesis:

let a be object ; :: thesis:
assume a in dom c1 ; :: thesis:
then reconsider j = a as Element of I ;
assume c1 . a <> c2 . a ; :: thesis:
then j in { i where i is Element of I : c1 . i <> c2 . i } ;
hence contradiction by A56; :: thesis:

end;

dom c1 = I by PARTFUN1:def 2
.= 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:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A54, A5);
then A58: S₁[ diff (b1,b2)] ;
assume indx b1 = indx b2 ; :: thesis:
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:
thus ( D . 1 = B1 & D . (len D) = B2 ) by A3, A4, A59; :: thesis:
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:

end;

given D being FinSequence of bool the carrier of (Segre_Product A) 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:
defpred S₁[ 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:

let k be Nat; :: thesis:
assume A66: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A67: product bb = D . (k + 1) ; :: thesis:
A68: k + 1 in dom D by A67, FUNCT_1:def 2;
then A69: k + 1 <= len D by FINSEQ_3:25;

per cases ;

suppose k = 0 ; :: thesis:

hence indx b1 = indx bb by A3, A61, A67, PUA2MSS1:2; :: thesis:

end;

suppose 0 < k ; :: thesis:

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:

end;

A73: S₁[ 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:
assume product bb = D . 0 ; :: thesis:
hence indx b1 = indx bb by A74, FUNCT_1:def 2; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A73, A65);
hence indx b1 = indx b2 by A4, A62; :: thesis: