:: deftheorem defines \for AOFA_L00:def 32 :
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 empty-yielding GeneratorSet of T
for S being non empty non void b₂ -extension b₁ PC-correct QC-correct QCLangSignature over Union X
for Y being empty-yielding b₄ -tolerating ManySortedSet of the carrier of S
for L being Language of Y,S
for A being Formula of L
for x, y, z being Element of Union X holds \for (x,y,z,A) = \for (x,y,(\for (z,A)));