theorem :: PENCIL_1:10
for I being non empty set
for A being ManySortedSet of I
for i, S being set holds {A} +* (i,S) is Segre-like