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

now

assume indx A <> j ; :: thesis: contradiction
then A . (indx A) is trivial by A2;
hence contradiction by Def21; :: thesis: verum

end;

hence ( not A . i is empty & A . i is trivial ) by A1, A2; :: thesis: verum