:: deftheorem Def4 defines transl MSUALG_6:def 4 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for i being Nat
for A being MSAlgebra over S
for a, b₆ being Function holds
( b₆ = transl (o,i,a,A) iff ( dom b₆ = the Sorts of A . ((the_arity_of o) /. i) & ( for x being object st x in the Sorts of A . ((the_arity_of o) /. i) holds
b₆ . x = (Den (o,A)) . (a +* (i,x)) ) ) );