A1: for x being variable holds P₁[x -term F₁()] and
A2: for c being constructor OperSymbol of F₁()
for p being FinSequence of QuasiTerms F₁() st len p = len (the_arity_of c) & ( for t being quasi-term of F₁() st t in rng p holds
P₁[t] ) holds
P₁[c -trm p] and
A3: for a being expression of F₁(), an_Adj F₁() st P₁[a] holds
P₁[(non_op F₁()) term a] and
A4: for a being expression of F₁(), an_Adj F₁() st P₁[a] holds
for t being expression of F₁(), a_Type F₁() st P₁[t] holds
P₁[(ast F₁()) term (a,t)]