:: deftheorem defines subst-correct AOFA_L00:def 16 :
for J being non empty non void Signature
for X being V3() ManySortedSet of the carrier of J
for Q being non-empty SubstMSAlgebra over J,X holds
( Q is subst-correct iff for x being Element of Union X
for a being SortSymbol of J st x in X . a holds
( ( for j being SortSymbol of J
for A being Element of Q,j holds A / (x,x) = A ) & ( for y being Element of Union the Sorts of Q st y in the Sorts of Q . a holds
for o being OperSymbol of J
for p being Element of Args (o,Q)
for A being Element of Q,(the_result_sort_of o) st A = (Den (o,Q)) . p & ( for S being QCLangSignature over Union X holds
( not J = S or for z being Element of Union X
for q being Element of {1,2} holds not o = the quantifiers of S . (q,z) ) ) holds
A / (x,y) = (Den (o,Q)) . (p / (x,y)) ) ) );