scheme :: MSAFREE5:sch 3
TermAlgebraInd{ P₁[ set ], F₁() -> non empty non void ManySortedSign , F₂() -> V5() ManySortedSet of the carrier of F₁(), F₃() -> F₂(),F₁() -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over F₁(), F₄() -> Element of F₃() } :

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