:: deftheorem defines vf-finite AOFA_L00:def 36 :
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 non-empty Language of Y,S holds
( L is vf-finite iff for s being SortSymbol of S
for t being Element of L,s holds vf t is V31() );