ex f being term-transformation of F₁(), MSVars F₁() st
( ( for x being variable holds f . (x -term F₁()) = F₂(x) ) & ( for c being constructor OperSymbol of F₁()
for p, q being FinSequence of QuasiTerms F₁() st len p = len (the_arity_of c) & q = f * p holds
f . (c -trm p) = F₄(c,q) ) & ( for a being expression of F₁(), an_Adj F₁() holds f . ((non_op F₁()) term a) = F₃((f . a)) ) & ( for a being expression of F₁(), an_Adj F₁()
for t being expression of F₁(), a_Type F₁() holds f . ((ast F₁()) term (a,t)) = F₅((f . a),(f . t)) ) )

A1: for x being variable holds F₂(x) is quasi-term of 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) holds
F₄(c,p) is expression of F₁(), the_result_sort_of c and
A3: for a being expression of F₁(), an_Adj F₁() holds F₃(a) is expression of F₁(), an_Adj F₁() and
A4: for a being expression of F₁(), an_Adj F₁()
for t being expression of F₁(), a_Type F₁() holds F₅(a,t) is expression of F₁(), a_Type F₁()