scheme :: MSAFREE4:sch 4
TermDefUniq{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty ManySortedSet of F₁(), F₃( set , set ) -> set , F₄( set , FinSequence) -> set , F₅() -> ManySortedSet of F₁() -Terms F₂(), F₆() -> ManySortedSet of F₁() -Terms F₂() } :

F₅() = F₆()

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds F₅() . (root-tree [x,s]) = F₃(x,s) and
A2: 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)) and
A3: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds F₆() . (root-tree [x,s]) = F₃(x,s) and
A4: 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))