theorem :: MSSUBFAM:17

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of I st A is_transformable_to B & F is ManySortedFunction of A,B holds
( doms F = A & rngs F c= B )