let I be non empty set ; :: thesis: for A being non trivial-yielding Segre-like ManySortedSet of I
for i being Element of I st i <> indx A holds
A . i is 1 -element
let A be non trivial-yielding Segre-like ManySortedSet of I; :: thesis: for i being Element of I st i <> indx A holds
A . i is 1 -element
let i be Element of I; :: thesis: ( i <> indx A implies A . i is 1 -element )
consider j being Element of I such that
A1: for k being Element of I st k <> j holds
A . k is 1 -element by Def20;

A2: now :: thesis: not indx A <> j

assume indx A <> j ; :: thesis: contradiction
then A . (indx A) is 1 -element by A1;
hence contradiction by Def21; :: thesis: verum

end;

assume i <> indx A ; :: thesis: A . i is 1 -element
hence A . i is 1 -element by A1, A2; :: thesis: verum