:: deftheorem defines -vf-yielding AOFA_L00:def 9 :
for S being non empty non void Signature
for X being ManySortedSet of the carrier of S
for T being VarMSAlgebra over S holds
( T is X -vf-yielding iff the free-vars of T is ManySortedMSSet of the Sorts of T,X );