:: deftheorem Def3 defines TranslationRel MSUALG_6:def 3 :
for S being non empty non void ManySortedSign
for b₂ being Relation of the carrier of S holds
( b₂ = TranslationRel S iff for s1, s2 being SortSymbol of S holds
( [s1,s2] in b₂ 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 ) ) ) );