let I be non empty finite set ; 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; ( ( 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
; 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; ( 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
; 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; ( 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
; ( 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 ) ) ) )
( 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
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
(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 for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A6:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verumproof
let c1,
c2 be non
trivial-yielding Segre-like ManySortedSubset of
Carrier A;
( 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
;
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 )
;
suppose A20:
product c1 misses product c3
;
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 ) ) )
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;
reconsider D =
E ^' F as
FinSequence of
bool the
carrier of
(Segre_Product A) ;
take
D
;
( 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;
( 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;
( ( 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 )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 )
verumproof
let i be
Nat;
( 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
;
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;
( 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)
;
( 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
i >= len E
;
( 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
;
( 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;
verum end; end; end; end;
end; end; suppose A53:
product c1 meets product c3
;
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 ) ) )
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;
verum end; end;
end; end;
A54:
S1[
0 ]
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
;
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
;
( 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;
( ( 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;
verum
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 )
; 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 for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A66:
S1[
k]
;
S1[k + 1]thus
S1[
k + 1]
verum end;
A73:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A73, A65);
hence
indx b1 = indx b2
by A4, A62; verum