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₁[ 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₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j < len f & S₁[j] implies S₁[j + 1] )
assume that
A14: 1 <= j and
A15: j < len f ; :: thesis: ( not S₁[j] or S₁[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₁[j] ; :: thesis: S₁[j + 1]
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 ) )

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

proof

let i be object ; :: thesis: ( i <> indx X1 implies X1 . i = H . i )
assume A24: i <> indx X1 ; :: thesis: X1 . i = H . i
then A25: i <> indx B1 by A21, A20;
thus X1 . i = B1 . i by A21, A20, A24
.= H . i by A20, A19, A23, A25, PENCIL_1:26 ; :: thesis: verum

end;

end;

hence S₁[j + 1] ; :: thesis: verum

end;

A26: S₁[1] by A10, A4, PUA2MSS1:2;
for i being Element of NAT st 1 <= i & i <= len f holds
S₁[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