:: deftheorem defines Eval MSAFREE2:def 9 :
for S being non empty non void ManySortedSign
for MSA being non-empty MSAlgebra over S
for b₃ being ManySortedFunction of (FreeEnv MSA),MSA holds
( b₃ = Eval MSA iff ( b₃ is_homomorphism FreeEnv MSA,MSA & ( for s being SortSymbol of S
for x, y being set st y in FreeSort ( the Sorts of MSA,s) & y = root-tree [x,s] & x in the Sorts of MSA . s holds
(b₃ . s) . y = x ) ) );