:: deftheorem ABBR defines . MSAFREE5:def 12 :
for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for f being ManySortedFunction of A,B st A is disjoint_valued holds
for a being Element of A holds f . a = (f . (the_sort_of a)) . a;