deffunc H₂( variable) -> Element of Union the Sorts of (Free (C,(MSVars C))) = IFIN ($1,(dom f),(f /. $1),($1 -term C));
deffunc H₃( constructor OperSymbol of C, FinSequence of QuasiTerms C) -> compound expression of C = $1 -trm $2;
deffunc H₄( expression of C) -> expression of C = (non_op C) term $1;
deffunc H₅( expression of C, expression of C) -> expression of C = (ast C) term ($1,$2);
A1: for x being variable holds H₂(x) is quasi-term of C

proof

let x be variable; :: thesis: H₂(x) is quasi-term of C
f /. x is quasi-term of C by Th41;
hence H₂(x) is quasi-term of C by MATRIX_7:def 1; :: thesis: verum

end;

A2: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
H₃(c,p) is expression of C, the_result_sort_of c by Th52;
A3: for a being expression of C, an_Adj C holds H₄(a) is expression of C, an_Adj C by Th43;
A4: for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds H₅(a,t) is expression of C, a_Type C by Th46;
consider f9 being term-transformation of C, MSVars C such that
A5: ( ( for x being variable holds f9 . (x -term C) = H₂(x) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f9 * p holds
f9 . (c -trm p) = H₃(c,q) ) & ( for a being expression of C, an_Adj C holds f9 . ((non_op C) term a) = H₄(f9 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f9 . ((ast C) term (a,t)) = H₅(f9 . a,f9 . t) ) ) from ABCMIZ_1:sch 3(A1, A2, A3, A4);
take f9 ; :: thesis: ( ( for x being variable holds
( ( x in dom f implies f9 . (x -term C) = f . x ) & ( not x in dom f implies f9 . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f9 * p holds
f9 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f9 . ((non_op C) term a) = (non_op C) term (f9 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f9 . ((ast C) term (a,t)) = (ast C) term ((f9 . a),(f9 . t)) ) )

hereby :: thesis: ( ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f9 * p holds
f9 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f9 . ((non_op C) term a) = (non_op C) term (f9 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f9 . ((ast C) term (a,t)) = (ast C) term ((f9 . a),(f9 . t)) ) )

let x be variable; :: thesis: ( ( x in dom f implies f9 . (x -term C) = f . x ) & ( not x in dom f implies f9 . (x -term C) = x -term C ) )
A6: f9 . (x -term C) = H₂(x) by A5;
( x in dom f implies f /. x = f . x ) by PARTFUN1:def 6;
hence ( x in dom f implies f9 . (x -term C) = f . x ) by A6, MATRIX_7:def 1; :: thesis: ( not x in dom f implies f9 . (x -term C) = x -term C )
thus ( not x in dom f implies f9 . (x -term C) = x -term C ) by A6, MATRIX_7:def 1; :: thesis: verum

end;

thus ( ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = f9 * p holds
f9 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f9 . ((non_op C) term a) = (non_op C) term (f9 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f9 . ((ast C) term (a,t)) = (ast C) term ((f9 . a),(f9 . t)) ) ) by A5; :: thesis: verum