:: deftheorem Def1 defines -MSF CATALG_1:def 1 :
for I being set
for A, f being Function
for b₄ being ManySortedFunction of I holds
( b₄ = f -MSF (I,A) iff for i being object st i in I holds
b₄ . i = f | (A . i) );