:: deftheorem Def14 defines / AOFA_L00:def 14 :
for J being non empty non void Signature
for X being empty-yielding ManySortedSet of the carrier of J
for Q being non-empty SubstMSAlgebra over J,X
for o being OperSymbol of J
for p being Element of Args (o,Q)
for x being Element of Union X
for y being Element of Union the Sorts of Q
for b₈ being Element of Args (o,Q) holds
( b₈ = p / (x,y) iff for i being Nat st i in dom (the_arity_of o) holds
ex j being SortSymbol of J st
( j = (the_arity_of o) . i & ex A being Element of Q,j st
( A = p . i & b₈ . i = A / (x,y) ) ) );