set V = MSVars F1();
set X = (MSVars F1()) \/ ( the carrier of F1() --> {0});
set A = Free (F1(),(MSVars F1()));
set U = the Sorts of (Free (F1(),(MSVars F1())));
set D = Union the Sorts of (Free (F1(),(MSVars F1())));
set G = DTConMSA (MSVars F1());
deffunc H2( Symbol of (DTConMSA (MSVars F1()))) -> expression of F1() = F2(($1 `1));
deffunc H3( Symbol of (DTConMSA (MSVars F1())), FinSequence, Function) -> Element of Union the Sorts of (Free (F1(),(MSVars F1()))) = IFEQ (($1 `1),*,F5(($3 . 1),($3 . 2)),(IFEQ (($1 `1),non_op,F3(($3 . 1)),F4(($1 `1),$3))));
consider f being Function of (TS (DTConMSA (MSVars F1()))),(Union the Sorts of (Free (F1(),(MSVars F1())))) such that
A5: for t being Symbol of (DTConMSA (MSVars F1())) st t in Terminals (DTConMSA (MSVars F1())) holds
f . (root-tree t) = H2(t) and
A6: for nt being Symbol of (DTConMSA (MSVars F1()))
for ts being FinSequence of TS (DTConMSA (MSVars F1())) st nt ==> roots ts holds
f . (nt -tree ts) = H3(nt, roots ts,f * ts) from DTCONSTR:sch 8();
 Union the Sorts of (Free (F1(),(MSVars F1()))) = TS (DTConMSA (MSVars F1())) by Th128;
then reconsider f = f as Function of (Union the Sorts of (Free (F1(),(MSVars F1())))),(Union the Sorts of (Free (F1(),(MSVars F1())))) ;
f is term-transformation of F1(), MSVars F1()
proof
let s be SortSymbol of F1(); :: according to ABCMIZ_1:def 56 :: thesis: f .: ( the Sorts of (Free (F1(),(MSVars F1()))) . s) c= the Sorts of (Free (F1(),(MSVars F1()))) . s
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: ( the Sorts of (Free (F1(),(MSVars F1()))) . s) or x in the Sorts of (Free (F1(),(MSVars F1()))) . s )
assume x in f .: ( the Sorts of (Free (F1(),(MSVars F1()))) . s) ; :: thesis: x in the Sorts of (Free (F1(),(MSVars F1()))) . s
then consider a being Element of Union the Sorts of (Free (F1(),(MSVars F1()))) such that
A7: a in the Sorts of (Free (F1(),(MSVars F1()))) . s and
A8: x = f . a by FUNCT_2:65;
defpred S1[ expression of F1()] means for s being SortSymbol of F1() st $1 in the Sorts of (Free (F1(),(MSVars F1()))) . s holds
f . $1 in the Sorts of (Free (F1(),(MSVars F1()))) . s;
A9: for x being variable holds S1[x -term F1()]
proof
let y be variable; :: thesis: S1[y -term F1()]
set a = y -term F1();
let s be SortSymbol of F1(); :: thesis: ( y -term F1() in the Sorts of (Free (F1(),(MSVars F1()))) . s implies f . (y -term F1()) in the Sorts of (Free (F1(),(MSVars F1()))) . s )
assume A10: y -term F1() in the Sorts of (Free (F1(),(MSVars F1()))) . s ; :: thesis: f . (y -term F1()) in the Sorts of (Free (F1(),(MSVars F1()))) . s
A11: [y,(a_Term F1())] in Terminals (DTConMSA (MSVars F1())) by Th122;
then reconsider t = [y,(a_Term F1())] as Symbol of (DTConMSA (MSVars F1())) ;
f . (y -term F1()) = H2(t) by A5, A11
.= F2(y) by MCART_1:7 ;
then A12: f . (y -term F1()) is quasi-term of F1() by A1;
y -term F1() is expression of F1(),s by A10, Def28;
then s = a_Term F1() by Th48;
hence f . (y -term F1()) in the Sorts of (Free (F1(),(MSVars F1()))) . s by A12, Def28; :: thesis: verum
end;
A13: for c being constructor OperSymbol of F1()
for p being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & ( for t being quasi-term of F1() st t in rng p holds
S1[t] ) holds
S1[c -trm p]
proof
let c be constructor OperSymbol of F1(); :: thesis: for p being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & ( for t being quasi-term of F1() st t in rng p holds
S1[t] ) holds
S1[c -trm p]
let p be FinSequence of QuasiTerms F1(); :: thesis: ( len p = len (the_arity_of c) & ( for t being quasi-term of F1() st t in rng p holds
S1[t] ) implies S1[c -trm p] )
assume that
A14: len p = len (the_arity_of c) and
A15: for t being quasi-term of F1() st t in rng p holds
S1[t] ; :: thesis: S1[c -trm p]
set a = c -trm p;
set nt = [c, the carrier of F1()];
let s be SortSymbol of F1(); :: thesis: ( c -trm p in the Sorts of (Free (F1(),(MSVars F1()))) . s implies f . (c -trm p) in the Sorts of (Free (F1(),(MSVars F1()))) . s )
assume A16: c -trm p in the Sorts of (Free (F1(),(MSVars F1()))) . s ; :: thesis: f . (c -trm p) in the Sorts of (Free (F1(),(MSVars F1()))) . s
[c, the carrier of F1()] in NonTerminals (DTConMSA (MSVars F1())) by Th123;
then reconsider nt = [c, the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) ;
reconsider ts = p as FinSequence of TS (DTConMSA (MSVars F1())) by Th128;
A17: c -trm p = nt -tree ts by A14, Def35;
reconsider aa = c -trm p as Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
the Sorts of (Free (F1(),(MSVars F1()))) = F1() -Terms ((MSVars F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by MSAFREE3:24;
then the Sorts of (Free (F1(),(MSVars F1()))) c= the Sorts of (FreeMSA ((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by PBOOLE:def 18;
then the Sorts of (Free (F1(),(MSVars F1()))) . s c= the Sorts of (FreeMSA ((MSVars F1()) \/ ( the carrier of F1() --> {0}))) . s by PBOOLE:def 2;
then aa in (FreeSort ((MSVars F1()) \/ ( the carrier of F1() --> {0}))) . s by A16;
then aa in FreeSort (((MSVars F1()) \/ ( the carrier of F1() --> {0})),s) by MSAFREE:def 11;
then A18: the_sort_of aa = s by MSATERM:def 5;
A19: nt `1 = c by MCART_1:7;
A20: c <> * by Def11;
A21: c <> non_op by Def11;
A22: rng p c= QuasiTerms F1() by FINSEQ_1:def 4;
dom f = Union the Sorts of (Free (F1(),(MSVars F1()))) by FUNCT_2:def 1;
then A23: rng p c= dom f ;
rng (f * p) c= QuasiTerms F1()
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (f * p) or z in QuasiTerms F1() )
assume z in rng (f * p) ; :: thesis: z in QuasiTerms F1()
then consider i being set such that
A24: i in dom (f * p) and
A25: z = (f * p) . i by FUNCT_1:def 3;
i in dom p by A23, A24, RELAT_1:27;
then A26: p . i in rng p by FUNCT_1:def 3;
then reconsider pi1 = p . i as quasi-term of F1() by A22, Th41;
pi1 in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Term F1()) by Th41;
then f . pi1 in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Term F1()) by A15, A26;
hence z in QuasiTerms F1() by A24, A25, FUNCT_1:12; :: thesis: verum
end;
then reconsider q = f * p as FinSequence of QuasiTerms F1() by FINSEQ_1:def 4;
rng p c= F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) )
assume z in rng p ; :: thesis: z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
then z is Element of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) ; :: thesis: verum
end;
then reconsider r = p as FinSequence of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by FINSEQ_1:def 4;
A27: len q = len p by A23, FINSEQ_2:29;
c -trm p is Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
then A28: r is ArgumentSeq of Sym (c,((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by A17, MSATERM:1;
then A29: the_result_sort_of c = s by A17, A18, MSATERM:20;
Sym (c,((MSVars F1()) \/ ( the carrier of F1() --> {0}))) ==> roots r by A28, MSATERM:21;
then nt ==> roots ts by Th127;
then f . (c -trm p) = H3(nt, roots ts,f * ts) by A6, A17
.= IFEQ (c,non_op,F3(((f * ts) . 1)),F4(c,(f * ts))) by A19, A20, FUNCOP_1:def 8
.= F4(c,(f * ts)) by A21, FUNCOP_1:def 8 ;
then f . (c -trm p) is expression of F1(), the_result_sort_of c by A2, A14, A27;
hence f . (c -trm p) in the Sorts of (Free (F1(),(MSVars F1()))) . s by A29, Def28; :: thesis: verum
end;
A30: for a being expression of F1(), an_Adj F1() st S1[a] holds
S1[(non_op F1()) term a]
proof
let v be expression of F1(), an_Adj F1(); :: thesis: ( S1[v] implies S1[(non_op F1()) term v] )
assume A31: S1[v] ; :: thesis: S1[(non_op F1()) term v]
A32: v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Def28;
then f . v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A31;
then reconsider fv = f . v as expression of F1(), an_Adj F1() by Def28;
let s be SortSymbol of F1(); :: thesis: ( (non_op F1()) term v in the Sorts of (Free (F1(),(MSVars F1()))) . s implies f . ((non_op F1()) term v) in the Sorts of (Free (F1(),(MSVars F1()))) . s )
assume A33: (non_op F1()) term v in the Sorts of (Free (F1(),(MSVars F1()))) . s ; :: thesis: f . ((non_op F1()) term v) in the Sorts of (Free (F1(),(MSVars F1()))) . s
A34: (non_op F1()) term v is expression of F1(), an_Adj F1() by Th43;
(non_op F1()) term v is expression of F1(),s by A33, Def28;
then A35: s = an_Adj F1() by A34, Th48;
set QA = the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1());
rng <*v*> = {v} by FINSEQ_1:38;
then rng <*v*> c= the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A32, ZFMISC_1:31;
then reconsider p = <*v*> as FinSequence of the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by FINSEQ_1:def 4;
set c = non_op F1();
set a = (non_op F1()) term v;
set nt = [(non_op F1()), the carrier of F1()];
[(non_op F1()), the carrier of F1()] in NonTerminals (DTConMSA (MSVars F1())) by Th123;
then reconsider nt = [(non_op F1()), the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) ;
reconsider ts = p as FinSequence of TS (DTConMSA (MSVars F1())) by Th128;
A36: (non_op F1()) term v = nt -tree ts by Th43;
A37: nt `1 = non_op F1() by MCART_1:7;
dom f = Union the Sorts of (Free (F1(),(MSVars F1()))) by FUNCT_2:def 1;
then A38: f * p = <*fv*> by FINSEQ_2:34;
rng p c= F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) )
assume z in rng p ; :: thesis: z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
then z is expression of F1(), an_Adj F1() by Th41;
then z is Element of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) ; :: thesis: verum
end;
then reconsider r = p as FinSequence of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by FINSEQ_1:def 4;
(non_op F1()) term v is Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
then r is ArgumentSeq of Sym ((non_op F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by A36, MSATERM:1;
then Sym ((non_op F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f . ((non_op F1()) term v) = H3(nt, roots ts,f * ts) by A6, A36
.= IFEQ ((non_op F1()),non_op,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts))) by A37, FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8
.= F3(fv) by A38, FINSEQ_1:40 ;
then f . ((non_op F1()) term v) is expression of F1(), an_Adj F1() by A3;
hence f . ((non_op F1()) term v) in the Sorts of (Free (F1(),(MSVars F1()))) . s by A35, Def28; :: thesis: verum
end;
A39: for a being expression of F1(), an_Adj F1() st S1[a] holds
for t being expression of F1(), a_Type F1() st S1[t] holds
S1[(ast F1()) term (a,t)]
proof
let v be expression of F1(), an_Adj F1(); :: thesis: ( S1[v] implies for t being expression of F1(), a_Type F1() st S1[t] holds
S1[(ast F1()) term (v,t)] )
assume A40: S1[v] ; :: thesis: for t being expression of F1(), a_Type F1() st S1[t] holds
S1[(ast F1()) term (v,t)]
let t be expression of F1(), a_Type F1(); :: thesis: ( S1[t] implies S1[(ast F1()) term (v,t)] )
assume A41: S1[t] ; :: thesis: S1[(ast F1()) term (v,t)]
A42: v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Def28;
A43: t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by Def28;
A44: f . v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A40, A42;
A45: f . t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by A41, A43;
reconsider fv = f . v as expression of F1(), an_Adj F1() by A44, Def28;
reconsider ft = f . t as expression of F1(), a_Type F1() by A45, Def28;
let s be SortSymbol of F1(); :: thesis: ( (ast F1()) term (v,t) in the Sorts of (Free (F1(),(MSVars F1()))) . s implies f . ((ast F1()) term (v,t)) in the Sorts of (Free (F1(),(MSVars F1()))) . s )
assume A46: (ast F1()) term (v,t) in the Sorts of (Free (F1(),(MSVars F1()))) . s ; :: thesis: f . ((ast F1()) term (v,t)) in the Sorts of (Free (F1(),(MSVars F1()))) . s
A47: (ast F1()) term (v,t) is expression of F1(), a_Type F1() by Th46;
(ast F1()) term (v,t) is expression of F1(),s by A46, Def28;
then A48: s = a_Type F1() by A47, Th48;
reconsider p = <*v,t*> as FinSequence of Union the Sorts of (Free (F1(),(MSVars F1()))) ;
set c = ast F1();
set a = (ast F1()) term (v,t);
set nt = [(ast F1()), the carrier of F1()];
[(ast F1()), the carrier of F1()] in NonTerminals (DTConMSA (MSVars F1())) by Th123;
then reconsider nt = [(ast F1()), the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) ;
reconsider ts = p as FinSequence of TS (DTConMSA (MSVars F1())) by Th128;
A49: (ast F1()) term (v,t) = nt -tree ts by Th46;
A50: nt `1 = ast F1() by MCART_1:7;
A51: f * p = <*fv,ft*> by FINSEQ_2:36;
rng p c= F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) )
assume z in rng p ; :: thesis: z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
then z is Element of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) ; :: thesis: verum
end;
then reconsider r = p as FinSequence of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by FINSEQ_1:def 4;
(ast F1()) term (v,t) is Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
then r is ArgumentSeq of Sym ((ast F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by A49, MSATERM:1;
then Sym ((ast F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f . ((ast F1()) term (v,t)) = H3(nt, roots ts,f * ts) by A6, A49
.= F5(((f * ts) . 1),((f * ts) . 2)) by A50, FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by A51, FINSEQ_1:44
.= F5(fv,ft) by A51, FINSEQ_1:44 ;
then f . ((ast F1()) term (v,t)) is expression of F1(), a_Type F1() by A4;
hence f . ((ast F1()) term (v,t)) in the Sorts of (Free (F1(),(MSVars F1()))) . s by A48, Def28; :: thesis: verum
end;
S1[a] from ABCMIZ_1:sch 2(A9, A13, A30, A39);
hence x in the Sorts of (Free (F1(),(MSVars F1()))) . s by A7, A8; :: thesis: verum
end;
then reconsider f = f as term-transformation of F1(), MSVars F1() ;
take f ; :: thesis: ( ( for x being variable holds f . (x -term F1()) = F2(x) ) & ( for c being constructor OperSymbol of F1()
for p, q being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & q = f * p holds
f . (c -trm p) = F4(c,q) ) & ( for a being expression of F1(), an_Adj F1() holds f . ((non_op F1()) term a) = F3((f . a)) ) & ( for a being expression of F1(), an_Adj F1()
for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (a,t)) = F5((f . a),(f . t)) ) )
hereby :: thesis: ( ( for c being constructor OperSymbol of F1()
for p, q being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & q = f * p holds
f . (c -trm p) = F4(c,q) ) & ( for a being expression of F1(), an_Adj F1() holds f . ((non_op F1()) term a) = F3((f . a)) ) & ( for a being expression of F1(), an_Adj F1()
for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (a,t)) = F5((f . a),(f . t)) ) )
let x be variable; :: thesis: f . (x -term F1()) = F2(x)
x in Vars ;
then A52: x in (MSVars F1()) . (a_Term F1()) by Def25;
reconsider x9 = x as Element of (MSVars F1()) . (a_Term F1()) by Def25;
reconsider xx = [x9,(a_Term F1())] as Symbol of (DTConMSA (MSVars F1())) by A52, MSAFREE3:2;
xx in Terminals (DTConMSA (MSVars F1())) by A52, MSAFREE:7;
hence f . (x -term F1()) = F2((xx `1)) by A5
.= F2(x) by MCART_1:7 ;
:: thesis: verum
end;
hereby :: thesis: ( ( for a being expression of F1(), an_Adj F1() holds f . ((non_op F1()) term a) = F3((f . a)) ) & ( for a being expression of F1(), an_Adj F1()
for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (a,t)) = F5((f . a),(f . t)) ) )
let c be constructor OperSymbol of F1(); :: thesis: for p, q being FinSequence of QuasiTerms F1() st len p = len (the_arity_of c) & q = f * p holds
f . (c -trm p) = F4(c,q)
let p, q be FinSequence of QuasiTerms F1(); :: thesis: ( len p = len (the_arity_of c) & q = f * p implies f . (c -trm p) = F4(c,q) )
assume that
A53: len p = len (the_arity_of c) and
A54: q = f * p ; :: thesis: f . (c -trm p) = F4(c,q)
set a = c -trm p;
set nt = [c, the carrier of F1()];
[c, the carrier of F1()] in NonTerminals (DTConMSA (MSVars F1())) by Th123;
then reconsider nt = [c, the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) ;
reconsider ts = p as FinSequence of TS (DTConMSA (MSVars F1())) by Th128;
A55: c -trm p = nt -tree ts by A53, Def35;
A56: nt `1 = c by MCART_1:7;
A57: c <> * by Def11;
A58: c <> non_op by Def11;
rng p c= F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) )
assume z in rng p ; :: thesis: z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
then z is Element of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) ; :: thesis: verum
end;
then reconsider r = p as FinSequence of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by FINSEQ_1:def 4;
c -trm p is Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
then r is ArgumentSeq of Sym (c,((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by A55, MSATERM:1;
then Sym (c,((MSVars F1()) \/ ( the carrier of F1() --> {0}))) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f . (c -trm p) = H3(nt, roots ts,f * ts) by A6, A55
.= IFEQ (c,non_op,F3(((f * ts) . 1)),F4(c,(f * ts))) by A56, A57, FUNCOP_1:def 8
.= F4(c,(f * ts)) by A58, FUNCOP_1:def 8 ;
hence f . (c -trm p) = F4(c,q) by A54; :: thesis: verum
end;
hereby :: thesis: for a being expression of F1(), an_Adj F1()
for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (a,t)) = F5((f . a),(f . t))
let v be expression of F1(), an_Adj F1(); :: thesis: f . ((non_op F1()) term v) = F3((f . v))
A59: v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Def28;
then f . v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Th129;
then reconsider fv = f . v as expression of F1(), an_Adj F1() by Def28;
set QA = the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1());
rng <*v*> = {v} by FINSEQ_1:38;
then rng <*v*> c= the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A59, ZFMISC_1:31;
then reconsider p = <*v*> as FinSequence of the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by FINSEQ_1:def 4;
set c = non_op F1();
set a = (non_op F1()) term v;
set nt = [(non_op F1()), the carrier of F1()];
[(non_op F1()), the carrier of F1()] in NonTerminals (DTConMSA (MSVars F1())) by Th123;
then reconsider nt = [(non_op F1()), the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) ;
reconsider ts = p as FinSequence of TS (DTConMSA (MSVars F1())) by Th128;
A60: (non_op F1()) term v = nt -tree ts by Th43;
A61: nt `1 = non_op F1() by MCART_1:7;
dom f = Union the Sorts of (Free (F1(),(MSVars F1()))) by FUNCT_2:def 1;
then A62: f * p = <*fv*> by FINSEQ_2:34;
rng p c= F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) )
assume z in rng p ; :: thesis: z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
then z is expression of F1(), an_Adj F1() by Th41;
then z is Element of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) ; :: thesis: verum
end;
then reconsider r = p as FinSequence of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by FINSEQ_1:def 4;
(non_op F1()) term v is Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
then r is ArgumentSeq of Sym ((non_op F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by A60, MSATERM:1;
then Sym ((non_op F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f . ((non_op F1()) term v) = H3(nt, roots ts,f * ts) by A6, A60
.= IFEQ ((non_op F1()),non_op,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts))) by A61, FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8 ;
hence f . ((non_op F1()) term v) = F3((f . v)) by A62, FINSEQ_1:40; :: thesis: verum
end;
let v be expression of F1(), an_Adj F1(); :: thesis: for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (v,t)) = F5((f . v),(f . t))
let t be expression of F1(), a_Type F1(); :: thesis: f . ((ast F1()) term (v,t)) = F5((f . v),(f . t))
A63: v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Def28;
A64: t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by Def28;
A65: f . v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A63, Th129;
A66: f . t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by A64, Th129;
reconsider fv = f . v as expression of F1(), an_Adj F1() by A65, Def28;
reconsider ft = f . t as expression of F1(), a_Type F1() by A66, Def28;
reconsider p = <*v,t*> as FinSequence of Union the Sorts of (Free (F1(),(MSVars F1()))) ;
set c = ast F1();
set a = (ast F1()) term (v,t);
set nt = [(ast F1()), the carrier of F1()];
[(ast F1()), the carrier of F1()] in NonTerminals (DTConMSA (MSVars F1())) by Th123;
then reconsider nt = [(ast F1()), the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) ;
reconsider ts = p as FinSequence of TS (DTConMSA (MSVars F1())) by Th128;
A67: (ast F1()) term (v,t) = nt -tree ts by Th46;
A68: nt `1 = ast F1() by MCART_1:7;
A69: f * p = <*fv,ft*> by FINSEQ_2:36;
rng p c= F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
proof
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) )
assume z in rng p ; :: thesis: z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0}))
then z is Element of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
hence z in F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) ; :: thesis: verum
end;
then reconsider r = p as FinSequence of F1() -Terms ((MSVars F1()) \/ ( the carrier of F1() --> {0})) by FINSEQ_1:def 4;
(ast F1()) term (v,t) is Term of F1(),((MSVars F1()) \/ ( the carrier of F1() --> {0})) by MSAFREE3:8;
then r is ArgumentSeq of Sym ((ast F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) by A67, MSATERM:1;
then Sym ((ast F1()),((MSVars F1()) \/ ( the carrier of F1() --> {0}))) ==> roots r by MSATERM:21;
then nt ==> roots ts by Th127;
then f . ((ast F1()) term (v,t)) = H3(nt, roots ts,f * ts) by A6, A67
.= F5(((f * ts) . 1),((f * ts) . 2)) by A68, FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by A69, FINSEQ_1:44 ;
hence f . ((ast F1()) term (v,t)) = F5((f . v),(f . t)) by A69, FINSEQ_1:44; :: thesis: verum