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