theorem :: MSAFREE4:14

for I being non empty set
for J being set
for A, B being ManySortedSet of I st A c= B holds
for f being Function of J,I holds A * f c= B * f