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 00: ( [o,the carrier of C] -tree p in Union the Sorts of (Free C,(MSVars C)) & q = (f # ) * p ) ; :: thesis: (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q
0D: 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 00;
0R: 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 CNSTR2;

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 ;
t = [c,the carrier of C] -tree p ;
then 01: ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) by Th83;
then reconsider p' = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
reconsider q' = (f # ) * p' as FinSequence of QuasiTerms C by ThTr2;
02: len q' = len p by ThTr2;
thus (f # ) . ([o,the carrier of C] -tree p) = (f # ) . (c -trm p') by 01, TERM
.= c -trm q' by 01, SUBST
.= [o,the carrier of C] -tree q by 00, 01, 02, TERM ; :: thesis: verum

end;

suppose X0: 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
X1: t = (ast C) term a,s by 0R, ThAst2;
a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by ELEMENT;
then (f # ) . a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by ThTr;
then reconsider fa = (f # ) . a as expression of C, an_Adj C by Th42;
s in the Sorts of (Free C,(MSVars C)) . (a_Type C) by ELEMENT;
then (f # ) . s in the Sorts of (Free C,(MSVars C)) . (a_Type C) by ThTr;
then reconsider fs = (f # ) . s as expression of C, a_Type C by Th42;
t = [(ast C),the carrier of C] -tree <*a,s*> by X1, ThAst;
then ( p = <*a,s*> & a in dom (f # ) & s in dom (f # ) ) by 0D, TREES_4:15;
then q = <*fa,fs*> by 00, FINSEQ_2:145;
then [o,the carrier of C] -tree q = (ast C) term fa,fs by X0, ThAst;
hence (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q by X1, SUBST; :: thesis: verum

end;

suppose X0: 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
X1: t = (non_op C) term a by 0R, ThNon2;
a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by ELEMENT;
then (f # ) . a in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by ThTr;
then reconsider fa = (f # ) . a as expression of C, an_Adj C by Th42;
t = [(non_op C),the carrier of C] -tree <*a*> by X1, ThNon;
then ( p = <*a*> & a in dom (f # ) ) by 0D, TREES_4:15;
then q = <*fa*> by 00, BAGORDER:3;
then [o,the carrier of C] -tree q = (non_op C) term fa by X0, ThNon;
hence (f # ) . ([o,the carrier of C] -tree p) = [o,the carrier of C] -tree q by X1, SUBST; :: thesis: verum

end;

end;