theorem Th12: :: PENCIL_1:12

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