for I being non empty set
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 ) )