:: deftheorem Def12 defines / AOFA_L00:def 12 :
for J being non empty non void Signature
for X being empty-yielding ManySortedSet of the carrier of J
for Q being SubstMSAlgebra over J,X st X is ManySortedSubset of the Sorts of Q holds
for j being SortSymbol of J st the Sorts of Q . j <> {} holds
for A being Element of Q,j
for x, y being Element of Union X st ex a being SortSymbol of J st
( x in X . a & y in X . a ) holds
A / (x,y) = the subst-op of Q . [A,[x,y]];