:: deftheorem Def6 defines # MSUALG_3:def 6 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for b₇ being Element of Args (o,U2) holds
( b₇ = F # x iff for n being Nat st n in dom x holds
b₇ . n = (F . ((the_arity_of o) /. n)) . (x . n) );