for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of A,B st f is "onto" holds
ex g being ManySortedFunction of B,A st f ** g = id B