:: deftheorem defines is_e.translation_of MSUALG_6:def 5 :
for S being non empty non void ManySortedSign
for s1, s2 being SortSymbol of S
for A being MSAlgebra over S
for f being Function holds
( f is_e.translation_of A,s1,s2 iff ex o being OperSymbol of S st
( the_result_sort_of o = s2 & ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args (o,A) & f = transl (o,i,a,A) ) ) ) );