:: deftheorem defines subst-correct3 AOFA_L00:def 21 :
for J being non empty non void Signature
for T being non-empty MSAlgebra over J
for X being V3() GeneratorSet of T
for S being non empty non void b₁ -extension QCLangSignature over Union X
for Y being V3() b₃ -tolerating ManySortedSet of the carrier of S
for L being non-empty LanguageStr over T,Y,S holds
( L is subst-correct3 iff for s, s1 being SortSymbol of S
for t being Element of L,s
for t1 being Element of L,s1
for y being Element of Union Y st y in Y . s holds
( y nin (vf t1) . s & ( y nin (vf t1) . s implies t1 / (y,t) = t1 ) & ( t1 = y & y in Y . s1 implies t1 / (y,t) = t ) & ( for x being Element of Union Y st x in Y . s holds
(t1 / (x,y)) / (y,x) = t1 ) ) );