theorem Th7: :: PENCIL_2:7

for I being non empty set
for A being 1-sorted-yielding ManySortedSet of I
for L being ManySortedSubset of Carrier A
for i being Element of I
for S being Subset of (A . i) holds L +* (i,S) is ManySortedSubset of Carrier A