:: deftheorem defines subst-eq-correct AOFA_L00:def 44 :
for n being non empty Nat
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 b₁ PC-correct QC-correct QCLangSignature over Union X
for L being non-empty Language of X extended_by ({}, the carrier of S),S holds
( L is subst-eq-correct iff for x0 being Element of Union (X extended_by ({}, the carrier of S))
for s, s1 being SortSymbol of S st x0 in X . s holds
for t being Element of L,s
for t1, t2 being Element of L,s1 holds (t1 '=' (t2,L)) / (x0,t) = (t1 / (x0,t)) '=' ((t2 / (x0,t)),L) );