theorem Th32: :: MSATERM:32

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 s being SortSymbol of S
for v being Element of V . s st t = root-tree [v,s] holds
root-tree ((f . s) . v) is_an_evaluation_of t,f