let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of I

for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds

for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds

for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

let X, Y be Subset of (Segre_Product A); :: thesis: ( not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable implies for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) ) )

assume that

A1: ( not X is trivial & X is closed_under_lines & X is strong ) and

A2: ( not Y is trivial & Y is closed_under_lines & Y is strong ) and

A3: X,Y are_joinable ; :: thesis: for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

set B = bool the carrier of (Segre_Product A);

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

A4: X = f . 1 and

A5: Y = f . (len f) and

A6: for W being Subset of (Segre_Product A) st W in rng f holds

( W is closed_under_lines & W is strong ) and

A7: for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) by A3;

len f in dom f by A2, A5, FUNCT_1:def 2;

then A8: 1 <= len f by FINSEQ_3:25;

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

A9: X = product B0 and

for C being Subset of (A . (indx B0)) st C = B0 . (indx B0) holds

( C is strong & C is closed_under_lines ) by A1, PENCIL_1:29;

let X1, Y1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( X = product X1 & Y = product Y1 implies ( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) ) )

assume that

A10: X = product X1 and

A11: Y = product Y1 ; :: thesis: ( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

defpred S_{1}[ Element of NAT ] means for H being non trivial-yielding Segre-like ManySortedSubset of Carrier A st f . $1 = product H holds

( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) );

A12: B0 = X1 by A10, A9, PUA2MSS1:2;

A13: for j being Element of NAT st 1 <= j & j < len f & S_{1}[j] holds

S_{1}[j + 1]
_{1}[1]
by A10, A4, PUA2MSS1:2;

for i being Element of NAT st 1 <= i & i <= len f holds

S_{1}[i]
from INT_1:sch 7(A26, A13);

hence ( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) ) by A11, A5, A8; :: thesis: verum

for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds

for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

let A be PLS-yielding ManySortedSet of I; :: thesis: for X, Y being Subset of (Segre_Product A) st not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable holds

for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

let X, Y be Subset of (Segre_Product A); :: thesis: ( not X is trivial & X is closed_under_lines & X is strong & not Y is trivial & Y is closed_under_lines & Y is strong & X,Y are_joinable implies for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) ) )

assume that

A1: ( not X is trivial & X is closed_under_lines & X is strong ) and

A2: ( not Y is trivial & Y is closed_under_lines & Y is strong ) and

A3: X,Y are_joinable ; :: thesis: for X1, Y1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A st X = product X1 & Y = product Y1 holds

( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

set B = bool the carrier of (Segre_Product A);

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

A4: X = f . 1 and

A5: Y = f . (len f) and

A6: for W being Subset of (Segre_Product A) st W in rng f holds

( W is closed_under_lines & W is strong ) and

A7: for i being Element of NAT st 1 <= i & i < len f holds

2 c= card ((f . i) /\ (f . (i + 1))) by A3;

len f in dom f by A2, A5, FUNCT_1:def 2;

then A8: 1 <= len f by FINSEQ_3:25;

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

A9: X = product B0 and

for C being Subset of (A . (indx B0)) st C = B0 . (indx B0) holds

( C is strong & C is closed_under_lines ) by A1, PENCIL_1:29;

let X1, Y1 be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( X = product X1 & Y = product Y1 implies ( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) ) )

assume that

A10: X = product X1 and

A11: Y = product Y1 ; :: thesis: ( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) )

defpred S

( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) );

A12: B0 = X1 by A10, A9, PUA2MSS1:2;

A13: for j being Element of NAT st 1 <= j & j < len f & S

S

proof

A26:
S
let j be Element of NAT ; :: thesis: ( 1 <= j & j < len f & S_{1}[j] implies S_{1}[j + 1] )

assume that

A14: 1 <= j and

A15: j < len f ; :: thesis: ( not S_{1}[j] or S_{1}[j + 1] )

j in dom f by A14, A15, FINSEQ_3:25;

then A16: f . j in rng f by FUNCT_1:3;

A17: 1 <= j + 1 by NAT_1:11;

j + 1 <= len f by A15, NAT_1:13;

then j + 1 in dom f by A17, FINSEQ_3:25;

then f . (j + 1) in rng f by FUNCT_1:3;

then reconsider fj = f . j, fj1 = f . (j + 1) as Subset of (Segre_Product A) by A16;

A18: card (fj /\ fj1) c= card fj by CARD_1:11, XBOOLE_1:17;

A19: 2 c= card (fj /\ fj1) by A7, A14, A15;

then 2 c= card fj by A18;

then ( not fj is trivial & fj is closed_under_lines & fj is strong ) by A6, A16, PENCIL_1:4;

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

A20: fj = product B1 and

for C being Subset of (A . (indx B1)) st C = B1 . (indx B1) holds

( C is strong & C is closed_under_lines ) by PENCIL_1:29;

assume A21: S_{1}[j]
; :: thesis: S_{1}[j + 1]

then A22: indx B0 = indx B1 by A12, A20;

_{1}[j + 1]
; :: thesis: verum

end;assume that

A14: 1 <= j and

A15: j < len f ; :: thesis: ( not S

j in dom f by A14, A15, FINSEQ_3:25;

then A16: f . j in rng f by FUNCT_1:3;

A17: 1 <= j + 1 by NAT_1:11;

j + 1 <= len f by A15, NAT_1:13;

then j + 1 in dom f by A17, FINSEQ_3:25;

then f . (j + 1) in rng f by FUNCT_1:3;

then reconsider fj = f . j, fj1 = f . (j + 1) as Subset of (Segre_Product A) by A16;

A18: card (fj /\ fj1) c= card fj by CARD_1:11, XBOOLE_1:17;

A19: 2 c= card (fj /\ fj1) by A7, A14, A15;

then 2 c= card fj by A18;

then ( not fj is trivial & fj is closed_under_lines & fj is strong ) by A6, A16, PENCIL_1:4;

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

A20: fj = product B1 and

for C being Subset of (A . (indx B1)) st C = B1 . (indx B1) holds

( C is strong & C is closed_under_lines ) by PENCIL_1:29;

assume A21: S

then A22: indx B0 = indx B1 by A12, A20;

now :: thesis: for H being non trivial-yielding Segre-like ManySortedSubset of Carrier A st f . (j + 1) = product H holds

( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) )

hence
S( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) )

let H be non trivial-yielding Segre-like ManySortedSubset of Carrier A; :: thesis: ( f . (j + 1) = product H implies ( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) ) )

assume A23: f . (j + 1) = product H ; :: thesis: ( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) )

hence indx X1 = indx H by A12, A20, A22, A19, PENCIL_1:26; :: thesis: for i being object st i <> indx X1 holds

X1 . i = H . i

thus for i being object st i <> indx X1 holds

X1 . i = H . i :: thesis: verum

end;X1 . i = H . i ) ) )

assume A23: f . (j + 1) = product H ; :: thesis: ( indx X1 = indx H & ( for i being object st i <> indx X1 holds

X1 . i = H . i ) )

hence indx X1 = indx H by A12, A20, A22, A19, PENCIL_1:26; :: thesis: for i being object st i <> indx X1 holds

X1 . i = H . i

thus for i being object st i <> indx X1 holds

X1 . i = H . i :: thesis: verum

for i being Element of NAT st 1 <= i & i <= len f holds

S

hence ( indx X1 = indx Y1 & ( for i being object st i <> indx X1 holds

X1 . i = Y1 . i ) ) by A11, A5, A8; :: thesis: verum