scheme :: MSAFREE5:sch 2
TermInd{ P₁[ set ], F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of the carrier of F₁(), F₃() -> Element of (Free (F₁(),F₂())) } :

P₁[F₃()]

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₂() . s holds P₁[x -term ] and
A2: for o being OperSymbol of F₁()
for p being Element of Args (o,(Free (F₁(),F₂()))) st ( for t being Element of (Free (F₁(),F₂())) st t in rng p holds
P₁[t] ) holds
P₁[o -term p]