:: deftheorem defines \ex AOFA_L00:def 33 :
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 A being Formula of L
for x, y, z being Element of Union X holds \ex (x,y,z,A) = \ex (x,y,(\ex (z,A)));