let o be OperSymbol of C; :: according to ABCMIZ_1:def 57 :: thesis: for p, q being FinSequence of (Free C,(MSVars C)) st [o,the carrier of C] -tree p in Union the Sorts of (Free C,(MSVars C)) & q = (f # ) * p holds
(f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q
let p, q be FinSequence of (Free C,(MSVars C)); :: thesis: ( [o,the carrier of C] -tree p in Union the Sorts of (Free C,(MSVars C)) & q = (f # ) * p implies (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q )
assume that
A1: [o,the carrier of C] -tree p in Union the Sorts of (Free C,(MSVars C)) and
A2: q = (f # ) * p ; :: thesis: (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q
A3: dom (f # ) = Union the Sorts of (Free C,(MSVars C)) by FUNCT_2:def 1;
reconsider t = [o,the carrier of C] -tree p as expression of C by A1;
A4: t . {} = [o,the carrier of C] by TREES_4:def 4;
set V = (MSVars C) \/ (the carrier of C --> {0 });

per cases ( o is constructor or o = * or o = non_op ) by Def11;

suppose o is constructor ; :: thesis: (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q

then reconsider c = o as constructor OperSymbol of C ;
A5: t = [c,the carrier of C] -tree p ;
then A6: len p = len (the_arity_of c) by Th51;
p in (QuasiTerms C) * by A5, Th51;
then reconsider p9 = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
reconsider q9 = (f # ) * p9 as FinSequence of QuasiTerms C by Th130;
A7: len q9 = len p by Th130;
thus (f # ) . ([o,the carrier of C] -tree p) = (f # ) . (c -trm p9) by A6, Def35
.= c -trm q9 by A6, Def60
.= [o,the carrier of C] -tree q by A2, A6, A7, Def35 ; :: thesis: verum

end;

suppose A8: o = * ; :: thesis: (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q

then consider a being expression of C, an_Adj C, s being expression of C, a_Type C such that
A9: t = (ast C) term a,s by A4, Th58;
a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by Def28;
then (f # ) . a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by Th129;
then reconsider fa = (f # ) . a as expression of C, an_Adj C by Th41;
s in the Sorts of (Free C,(MSVars C)) . (a_Type C) by Def28;
then (f # ) . s in the Sorts of (Free C,(MSVars C)) . (a_Type C) by Th129;
then reconsider fs = (f # ) . s as expression of C, a_Type C by Th41;
t = [(ast C),the carrier of C] -tree <*a,s*> by A9, Th46;
then p = <*a,s*> by TREES_4:15;
then q = <*fa,fs*> by A2, A3, FINSEQ_2:145;
then [o,the carrier of C] -tree q = (ast C) term fa,fs by A8, Th46;
hence (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q by A9, Def60; :: thesis: verum

end;

suppose A10: o = non_op ; :: thesis: (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q

then consider a being expression of C, an_Adj C such that
A11: t = (non_op C) term a by A4, Th57;
a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by Def28;
then (f # ) . a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by Th129;
then reconsider fa = (f # ) . a as expression of C, an_Adj C by Th41;
t = [(non_op C),the carrier of C] -tree <*a*> by A11, Th43;
then p = <*a*> by TREES_4:15;
then q = <*fa*> by A2, A3, FINSEQ_2:38;
then [o,the carrier of C] -tree q = (non_op C) term fa by A10, Th43;
hence (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q by A11, Def60; :: thesis: verum

end;

end;