let I be non empty set ; :: thesis: for A being PLS-yielding ManySortedSet of
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 set st i <> indx X1 holds
X1 . i = Y1 . i ) )
let A be PLS-yielding ManySortedSet of ; :: 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 set 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 set 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 set st i <> indx X1 holds
X1 . i = Y1 . i ) )
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 set st i <> indx X1 holds
X1 . i = Y1 . i ) ) )
assume A4: ( X = product X1 & Y = product Y1 ) ; :: thesis: ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) )
consider B0 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A5: ( X = product B0 & ( 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;
A6: B0 = X1 by A4, A5, PUA2MSS1:2;
set B = bool the carrier of (Segre_Product A);
consider f being FinSequence of bool the carrier of (Segre_Product A) such that
A7: ( X = f . 1 & Y = f . (len f) & ( for W being Subset of (Segre_Product A) st W in rng f holds
( W is closed_under_lines & W is strong ) ) & ( for i being Element of NAT st 1 <= i & i < len f holds
2 c= card ((f . i) /\ (f . (i + 1))) ) ) by A3, Def3;
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 set st i <> indx X1 holds
X1 . i = H . i ) );
A8: S₁[1] by A4, A7, PUA2MSS1:2;
A9: 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 A10: ( 1 <= j & j < len f ) ; :: thesis: ( not S₁[j] or S₁[j + 1] )
then A11: j in dom f by FINSEQ_3:27;
A12: 1 <= j + 1 by NAT_1:11;
j + 1 <= len f by A10, NAT_1:13;
then j + 1 in dom f by A12, FINSEQ_3:27;
then A13: ( f . j in rng f & f . (j + 1) in rng f ) by A11, FUNCT_1:12;
then reconsider fj = f . j, fj1 = f . (j + 1) as Subset of (Segre_Product A) ;
A14: card (fj /\ fj1) c= card fj by CARD_1:27, XBOOLE_1:17;
assume A15: S₁[j] ; :: thesis: S₁[j + 1]
2 c= card (fj /\ fj1) by A7, A10;
then 2 c= card fj by A14, XBOOLE_1:1;
then ( not fj is trivial & fj is closed_under_lines & fj is strong ) by A7, A13, PENCIL_1:4;
then consider B1 being non trivial-yielding Segre-like ManySortedSubset of Carrier A such that
A16: ( fj = product B1 & ( 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;
A17: ( indx B0 = indx B1 & ( for i being set st i <> indx B0 holds
B0 . i = B1 . i ) ) by A6, A15, A16;
A18: 2 c= card (fj /\ fj1) by A7, A10;

now

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 set st i <> indx X1 holds
X1 . i = H . i ) ) )
assume A19: f . (j + 1) = product H ; :: thesis: ( indx X1 = indx H & ( for i being set st i <> indx X1 holds
X1 . i = H . i ) )
hence indx X1 = indx H by A6, A16, A17, A18, PENCIL_1:26; :: thesis: for i being set st i <> indx X1 holds
X1 . i = H . i
thus for i being set st i <> indx X1 holds
X1 . i = H . i :: thesis: verum

proof

let i be set ; :: thesis: ( i <> indx X1 implies X1 . i = H . i )
assume A20: i <> indx X1 ; :: thesis: X1 . i = H . i
then A21: i <> indx B1 by A15, A16;
thus X1 . i = B1 . i by A15, A16, A20
.= H . i by A16, A18, A19, A21, PENCIL_1:26 ; :: thesis: verum

end;

end;

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

end;

A22: for i being Element of NAT st 1 <= i & i <= len f holds
S₁[i] from POLYNOM2:sch 4(A8, A9);
len f in dom f by A2, A7, FUNCT_1:def 4;
then 1 <= len f by FINSEQ_3:27;
hence ( indx X1 = indx Y1 & ( for i being set st i <> indx X1 holds
X1 . i = Y1 . i ) ) by A4, A7, A22; :: thesis: verum