:: deftheorem defines vf AOFA_A00:def 9 :
for S being non empty non void ManySortedSign
for A being non-empty VarMSAlgebra over S
for a being SortSymbol of S
for t being Element of A,a holds vf t = ( the free-vars of A . a) . t;