scheme :: MSATERM:sch 2
CTermInd{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra over F₁(), F₃() -> V2() ManySortedSet of the carrier of F₁(), P₁[ set ] } :

for t being c-Term of F₂(),F₃() holds P₁[t]

provided

A1: for s being SortSymbol of F₁()
for x being Element of the Sorts of F₂() . s holds P₁[ root-tree [x,s]] and
A2: for s being SortSymbol of F₁()
for v being Element of F₃() . s holds P₁[ root-tree [v,s]] and
A3: for o being OperSymbol of F₁()
for p being ArgumentSeq of o,F₂(),F₃() st ( for t being c-Term of F₂(),F₃() st t in rng p holds
P₁[t] ) holds
P₁[(Sym (o,( the Sorts of F₂() (\/) F₃()))) -tree p]