:: deftheorem Def4 defines MSFuncs AUTALG_1:def 4 :
for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
MSFuncs (A,B) = product ((Funcs) (A,B));