deffunc H2( variable) -> Element of Union the Sorts of (Free (C,(MSVars C))) = IFIN ($1,(dom f),(f /. $1),($1 -term C));
deffunc H3( constructor OperSymbol of C, FinSequence of QuasiTerms C) -> compound expression of C = $1 -trm $2;
deffunc H4( expression of C) -> expression of C = (non_op C) term $1;
deffunc H5( expression of C, expression of C) -> expression of C = (ast C) term ($1,$2);
A1: for x being variable holds H2(x) is quasi-term of C
proof
let x be variable; :: thesis: H2(x) is quasi-term of C
f /. x is quasi-term of C by Th41;
hence H2(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
H3(c,p) is expression of C, the_result_sort_of c by Th52;
A3: for a being expression of C, an_Adj C holds H4(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 H5(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) = H2(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) = H3(c,q) ) & ( for a being expression of C, an_Adj C holds f9 . ((non_op C) term a) = H4(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)) = H5(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) = H2(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