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;
per cases ( o is constructor or o = * or o = non_op ) ;
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:125;
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:34;
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;