scheme :: MSAFREE4:sch 3
TermDefEx{ F1() -> non empty non void ManySortedSign , F2() -> V5() ManySortedSet of F1(), F3( set , set ) -> set , F4( set , set ) -> set } :
ex F being ManySortedSet of F1() -Terms F2() st
( ( for s being SortSymbol of F1()
for x being Element of F2() . s holds F . (root-tree [x,s]) = F3(x,s) ) & ( for o being OperSymbol of F1()
for p being ArgumentSeq of Sym (o,F2()) holds F . ((Sym (o,F2())) -tree p) = F4(o,(F * p)) ) )