:: deftheorem Def7 defines # MSUALG_4:def 7 :
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S
for R being MSCongruence of A
for x being Element of Args (o,A)
for b₆ being Element of product ((Class R) * (the_arity_of o)) holds
( b₆ = R # x iff for n being Nat st n in dom (the_arity_of o) holds
b₆ . n = Class ((R . ((the_arity_of o) /. n)),(x . n)) );