:: deftheorem Def10 defines @ MSATERM:def 10 :
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A
for b₆ being Element of the Sorts of A . (the_sort_of t) holds
( b₆ = t @ f iff ex vt being finite DecoratedTree st
( vt is_an_evaluation_of t,f & b₆ = vt . {} ) );