theorem :: AUTALG_1:10

for I being set
for A, B, C being ManySortedSet of I st A is_transformable_to B & B is_transformable_to C holds
A is_transformable_to C