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
( ( x in dom f or not x in dom f ) & f /. x is quasi-term of C & x -term C is quasi-term of C ) by Th42;
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 Th43c;
A3: for a being expression of C, an_Adj C holds H₄(a) is expression of C, an_Adj C by ThNon;
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 ThAst;
consider f' being term-transformation of C, MSVars C such that
A5: ( ( for x being variable holds f' . (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 = f' * p holds
f' . (c -trm p) = H₃(c,q) ) & ( for a being expression of C, an_Adj C holds f' . ((non_op C) term a) = H₄(f' . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f' . ((ast C) term a,t) = H₅(f' . a,f' . t) ) ) from ABCMIZ_1:sch 3(A1, A2, A3, A4);
take f' ; :: thesis: ( ( for x being variable holds
( ( x in dom f implies f' . (x -term C) = f . x ) & ( not x in dom f implies f' . (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 = f' * p holds
f' . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f' . ((non_op C) term a) = (non_op C) term (f' . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f' . ((ast C) term a,t) = (ast C) term (f' . a),(f' . 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 = f' * p holds
f' . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f' . ((non_op C) term a) = (non_op C) term (f' . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f' . ((ast C) term a,t) = (ast C) term (f' . a),(f' . t) ) )

let x be variable; :: thesis: ( ( x in dom f implies f' . (x -term C) = f . x ) & ( not x in dom f implies f' . (x -term C) = x -term C ) )
A6: f' . (x -term C) = H₂(x) by A5;
( x in dom f implies f /. x = f . x ) by PARTFUN1:def 8;
hence ( x in dom f implies f' . (x -term C) = f . x ) by A6, MATRIX_7:def 1; :: thesis: ( not x in dom f implies f' . (x -term C) = x -term C )
thus ( not x in dom f implies f' . (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 = f' * p holds
f' . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds f' . ((non_op C) term a) = (non_op C) term (f' . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds f' . ((ast C) term a,t) = (ast C) term (f' . a),(f' . t) ) ) by A5; :: thesis: verum