for I being set
for A, B, C being ManySortedSet of I st A is_transformable_to B holds
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds G ** F is ManySortedFunction of A,C