scheme :: MSAFREE4:sch 3
TermDefEx{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty ManySortedSet of F₁(), F₃( set , set ) -> set , F₄( set , set ) -> set } :

ex F being ManySortedSet of F₁() -Terms F₂() st
( ( for s being SortSymbol of F₁()
for x being Element of F₂() . s holds F . (root-tree [x,s]) = F₃(x,s) ) & ( for o being OperSymbol of F₁()
for p being ArgumentSeq of Sym (o,F₂()) holds F . ((Sym (o,F₂())) -tree p) = F₄(o,(F * p)) ) )