:: deftheorem Def7 defines @ CIRCTRM1:def 7 :
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 DecoratedTree st t is Term of S,V holds
for f being ManySortedFunction of V, the Sorts of A
for b₆ being set holds
( b₆ = t @ (f,A) iff ex t9 being c-Term of A,V st
( t9 = t & b₆ = t9 @ f ) );