:: deftheorem defines '=' AOFA_L00:def 34 :
for n being natural non empty number
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 Y being V3() b₄ -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for t1, t2 being object st ex a being SortSymbol of J st
( t1 in the Sorts of T . a & t2 in the Sorts of T . a ) holds
t1 '=' (t2,L) = the equality of L . (t1,t2);