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
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
; ( ( 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)) ) )
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; verum