:: deftheorem defines subst-correct2 AOFA_L00:def 17 :
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-correct2 iff for j being SortSymbol of J
for q, t being Element of Q,j
for x being Element of Union X st t = x & x in X . j holds
t / (x,q) = q );