theorem :: MSUALG_9:6

for I being set
for A being ManySortedSet of I ex B being V2() ManySortedSet of I st A c= B