:: deftheorem defines vf-correct AOFA_A00:def 10 :
for S being non empty non void ManySortedSign
for A being non-empty VarMSAlgebra over S holds
( A is vf-correct iff for o being OperSymbol of S
for p being FinSequence st p in Args (o,A) holds
for b being Element of A,(the_result_sort_of o) st b = (Den (o,A)) . p holds
for s being SortSymbol of S holds (vf b) . s c= union { ((vf a) . s) where s0 is SortSymbol of S, a is Element of A,s0 : ex i being Nat st
( i in dom (the_arity_of o) & s0 = (the_arity_of o) . i & a = p . i ) } );