let I be non empty finite set ; :: thesis:
let A be PLS-yielding ManySortedSet of ; :: 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 A3: ( B1 = product b1 & 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

assume A4: indx b1 = indx b2 ; :: thesis:
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: S₁[ 0 ]

proof

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A6: ( 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 ) ; :: thesis:
A7: dom c1 = I by PARTFUN1:def 4
.= dom c2 by PARTFUN1:def 4 ;

now

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

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 A6, A7, FUNCT_1:9; :: thesis:

end;

A8: now

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

proof

let c1, c2 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A10: ( 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 ) ; :: thesis:
{ i where i is Element of I : c1 . i <> c2 . i } <> {} by A10;
then consider j0 being set 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
A12: ( j0 = j & c1 . j <> c2 . j ) by A11;
A13: ( c1 . (indx c1) = [#] (A . (indx c1)) & c2 . (indx c1) = [#] (A . (indx c1)) ) by A10, Th10;
then A14: j <> indx c1 by A12;
then ( not c1 . j is empty & c1 . j is trivial ) by PENCIL_1:12;
then consider p being set such that
A15: c1 . j = {p} by REALSET1:def 4;
c1 c= Carrier A by PBOOLE:def 23;
then {p} c= (Carrier A) . j by A15, PBOOLE:def 5;
then p in (Carrier A) . j by ZFMISC_1:37;
then p in [#] (A . j) by Th7;
then reconsider p = p as Point of (A . j) ;
( not c2 . j is empty & c2 . j is trivial ) by A10, A14, PENCIL_1:12;
then consider r being set such that
A16: c2 . j = {r} by REALSET1:def 4;
reconsider c3 = c2 +* j,{p} as non trivial-yielding Segre-like ManySortedSubset of Carrier A by A10, A14, Th13;
A17: product c3 is Subset of (Segre_Product A) by Th14;
A18: not A . (indx c1) is trivial by Th2;
A19: c3 . (indx c1) = [#] (A . (indx c1)) by A13, A14, FUNCT_7:34;
then not c3 . (indx c1) is trivial by A18;
then A20: indx c3 = indx c1 by PENCIL_1:def 21;
then A21: product c3 is Segre-Coset of A by A17, A19, PENCIL_2:def 2;

per cases ;

suppose A22: 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
A23: ( E . 1 = product c1 & E . (len E) = product c3 & ( for i being Nat st i in dom E holds
E . i is Segre-Coset of A ) & ( 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 A9, A10, A20, A21, A22;
not p in c2 . j by A12, A15, A16, TARSKI:def 1;
then consider F being FinSequence of bool the carrier of (Segre_Product A) such that
A24: ( F . 1 = product c3 & F . (len F) = product c2 & ( for i being Nat st i in dom F holds
F . i is Segre-Coset of A ) & ( 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, A10, A21, Th22;
reconsider D = E ^' F as FinSequence of bool the carrier of (Segre_Product A) ;
take D ; :: thesis:
1 in dom E by A23, FUNCT_1:def 4;
then 1 <= len E by FINSEQ_3:27;
hence D . 1 = product c1 by A23, GRAPH_2:14; :: thesis:
1 in dom F by A24, FUNCT_1:def 4;
then A25: 1 <= len F by FINSEQ_3:27;

now

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

end;

then A27: len F > 1 by A25, XXREAL_0:1;
hence D . (len D) = product c2 by A24, GRAPH_2:16; :: 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:
assume i in dom D ; :: thesis:
then A28: D . i in rng D by FUNCT_1:12;
A29: rng D c= (rng E) \/ (rng F) by GRAPH_2:17;

per cases by A28, A29, XBOOLE_0:def 3;

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

then consider i0 being set such that
A30: ( i0 in dom E & D . i = E . i0 ) by FUNCT_1:def 5;
reconsider i0 = i0 as Element of NAT by A30;
thus D . i is Segre-Coset of A by A23, A30; :: thesis:

end;

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

then consider i0 being set such that
A31: ( i0 in dom F & D . i = F . i0 ) by FUNCT_1:def 5;
reconsider i0 = i0 as Element of NAT by A31;
thus D . i is Segre-Coset of A by A24, A31; :: 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 A32: ( 1 <= i & i < len D ) ; :: thesis:
let Di, Di1 be Segre-Coset of A; :: thesis:
assume A33: ( Di = D . i & Di1 = D . (i + 1) ) ; :: thesis:
reconsider i = i as Element of NAT by ORDINAL1:def 13;

per cases ;

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

then A35: Di = E . i by A32, A33, GRAPH_2:14;
( 1 <= i + 1 & i + 1 <= len E ) by A34, NAT_1:11, NAT_1:13;
then Di1 = E . (i + 1) by A33, GRAPH_2:14;
hence ( Di misses Di1 & Di '||' Di1 ) by A23, A32, A34, A35; :: thesis:

end;

suppose i >= len E ; :: thesis:

then consider k being Nat such that
A36: i = (len E) + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A37: F <> {} by A25;

per cases ;

suppose k > 0 ; :: thesis:

then A38: 0 + 1 <= k by NAT_1:13;
((len E) + k) + 1 < (len D) + 1 by A32, A36, XREAL_1:8;
then A39: (len E) + (k + 1) < (len E) + (len F) by A37, GRAPH_2:13;
then A40: k + 1 < len F by XREAL_1:8;
then k < len F by NAT_1:13;
then A41: Di = F . (k + 1) by A33, A36, A38, GRAPH_2:15;
Di1 = D . ((len E) + (k + 1)) by A33, A36;
then A42: Di1 = F . ((k + 1) + 1) by A40, GRAPH_2:15, NAT_1:11;
( 1 <= k + 1 & k + 1 < len F ) by A39, NAT_1:11, XREAL_1:8;
hence ( Di misses Di1 & Di '||' Di1 ) by A24, A41, A42; :: thesis:

end;

suppose A43: k = 0 ; :: thesis:

then A44: Di = F . 1 by A23, A24, A32, A33, A36, GRAPH_2:14;
Di1 = F . (1 + 1) by A27, A33, A36, A43, GRAPH_2:15;
hence ( Di misses Di1 & Di '||' Di1 ) by A24, A27, A44; :: thesis:

end;

suppose product c1 meets product c3 ; :: thesis:

then A45: c1 = c3 by A10, A20, A21, Th11;
not p in c2 . j by A12, A15, A16, 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, A10, A45, Th22; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A8);
then S₁[ diff b1,b2] ;
then consider D being FinSequence of bool the carrier of (Segre_Product A) such that
A46: ( 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 ) ) ) by A2, A3, A4;
take D ; :: thesis:
thus ( D . 1 = B1 & D . (len D) = B2 ) by A3, A46; :: 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 A46; :: thesis:

end;

given D being FinSequence of bool the carrier of (Segre_Product A) such that A47: ( 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:
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;
A48: S₁[ 0 ]

proof

let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A49: product bb = D . 0 ; :: thesis:
not 0 in dom D by FINSEQ_3:26;
hence indx b1 = indx bb by A49, FUNCT_1:def 4; :: thesis:

end;

A50: now

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

proof

let bb be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis:
assume A52: product bb = D . (k + 1) ; :: thesis:
A53: k + 1 in dom D by A52, FUNCT_1:def 4;
then A54: ( 1 <= k + 1 & k + 1 <= len D ) by FINSEQ_3:27;

per cases ;

suppose k = 0 ; :: thesis:

hence indx b1 = indx bb by A3, A47, A52, PUA2MSS1:2; :: thesis:

end;

suppose 0 < k ; :: thesis:

then 0 + 1 < k + 1 by XREAL_1:8;
then A55: 1 <= k by NAT_1:13;
k <= len D by A54, NAT_1:13;
then k in dom D by A55, FINSEQ_3:27;
then reconsider B0 = D . k as Segre-Coset of A by A47;
reconsider B3 = D . (k + 1) as Segre-Coset of A by A47, A53;
consider b0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A56: ( B0 = product b0 & b0 . (indx b0) = [#] (A . (indx b0)) ) by PENCIL_2:def 2;
A57: indx b1 = indx b0 by A51, A56;
k < len D by A54, NAT_1:13;
then ( B0 misses B3 & B0 '||' B3 ) by A47, A55;
hence indx b1 = indx bb by A52, A56, A57, Th21; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A48, A50);
hence indx b1 = indx b2 by A3, A47; :: thesis: