for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A