theorem Th18: :: AUTALG_1:18

for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
(Funcs) (A,B) is V2()