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:116;
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:9;
the Sorts of (Free F1(),(MSVars F1())) = F1() -Terms (MSVars F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:25;
then the Sorts of (Free F1(),(MSVars F1())) c= the Sorts of (FreeMSA ((MSVars F1()) \/ (the carrier of F1() --> {0 }))) by PBOOLE:def 23;
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 5;
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 13;
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 5;
i in dom p by A23, A24, RELAT_1:46;
then A26: p . i in rng p by FUNCT_1:def 5;
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:22; :: 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:9;
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:33;
c -trm p is Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
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 A33: 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 A34: (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
A35: (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 A34, Def28;
then A36: s = an_Adj F1() by A35, Th48;
set QA = the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1());
rng <*v*> = {v} by FINSEQ_1:55;
then rng <*v*> c= the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A32, ZFMISC_1:37;
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;
A37: (non_op F1()) term v = nt -tree ts by Th43;
reconsider aa = (non_op F1()) term v as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
A38: 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 A39: f * p = <*fv*> by BAGORDER:3;
rng <*fv*> = {fv} by FINSEQ_1:55;
then rng <*fv*> c= the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A33, ZFMISC_1:37;
then reconsider q = f * p as FinSequence of the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A39, 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 expression of F1(), an_Adj F1() by Th41;
then z is Element of F1() -Terms ((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
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:9;
then r is ArgumentSeq of Sym (non_op F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by A37, 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, A37
.= IFEQ (non_op F1()),non_op ,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts)) by A38, FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8
.= F3(fv) by A39, FINSEQ_1:57 ;
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 A36, Def28; :: thesis: verum
end;
A40: 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 A41: 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 A42: S1[t] ; :: thesis: S1[(ast F1()) term v,t]
A43: v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by Def28;
A44: t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) by Def28;
A45: f . v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A41, A43;
A46: f . t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) by A42, A44;
reconsider fv = f . v as expression of F1(), an_Adj F1() by A45, Def28;
reconsider ft = f . t as expression of F1(), a_Type F1() by A46, 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 A47: (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
A48: (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 A47, Def28;
then A49: s = a_Type F1() by A48, Th48;
set QA = the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1());
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;
A50: (ast F1()) term v,t = nt -tree ts by Th46;
reconsider aa = (ast F1()) term v,t as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
A51: nt `1 = ast F1() by MCART_1:7;
A52: f * p = <*fv,ft*> by FINSEQ_2:40;
reconsider q = f * p as FinSequence of Union the Sorts of (Free F1(),(MSVars F1())) ;
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:9;
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:9;
then r is ArgumentSeq of Sym (ast F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by A50, 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, A50
.= F5(((f * ts) . 1),((f * ts) . 2)) by A51, FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by A52, FINSEQ_1:61
.= F5(fv,ft) by A52, FINSEQ_1:61 ;
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 A49, Def28; :: thesis: verum
end;
S1[a] from ABCMIZ_1:sch 2(A9, A13, A30, A40);
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 A53: 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 A53, MSAFREE3:3;
xx in Terminals (DTConMSA (MSVars F1())) by A53, 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)
the carrier of F1() in {the carrier of F1()} by TARSKI:def 1;
then [c,the carrier of F1()] in [:the carrier' of F1(),{the carrier of F1()}:] by ZFMISC_1:106;
then reconsider cc = [c,the carrier of F1()] as Symbol of (DTConMSA (MSVars F1())) by XBOOLE_0:def 3;
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
A54: len p = len (the_arity_of c) and
A55: 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;
A56: c -trm p = nt -tree ts by A54, Def35;
reconsider aa = c -trm p as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
A57: nt `1 = c by MCART_1:7;
A58: c <> * by Def11;
A59: 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:9;
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:9;
then r is ArgumentSeq of Sym c,((MSVars F1()) \/ (the carrier of F1() --> {0 })) by A56, 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, A56
.= IFEQ c,non_op ,F3(((f * ts) . 1)),F4(c,(f * ts)) by A57, A58, FUNCOP_1:def 8
.= F4(c,(f * ts)) by A59, FUNCOP_1:def 8 ;
hence f . (c -trm p) = F4(c,q) by A55; :: 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))
A60: v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by Def28;
then A61: 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:55;
then rng <*v*> c= the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A60, ZFMISC_1:37;
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;
A62: (non_op F1()) term v = nt -tree ts by Th43;
reconsider aa = (non_op F1()) term v as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
A63: 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 A64: f * p = <*fv*> by BAGORDER:3;
rng <*fv*> = {fv} by FINSEQ_1:55;
then rng <*fv*> c= the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A61, ZFMISC_1:37;
then reconsider q = f * p as FinSequence of the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A64, 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 expression of F1(), an_Adj F1() by Th41;
then z is Element of F1() -Terms ((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
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:9;
then r is ArgumentSeq of Sym (non_op F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by A62, 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, A62
.= IFEQ (non_op F1()),non_op ,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts)) by A63, FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8 ;
hence f . ((non_op F1()) term v) = F3((f . v)) by A64, FINSEQ_1:57; :: 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))
A65: v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by Def28;
A66: t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) by Def28;
A67: f . v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by A65, Th129;
A68: f . t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) by A66, Th129;
reconsider fv = f . v as expression of F1(), an_Adj F1() by A67, Def28;
reconsider ft = f . t as expression of F1(), a_Type F1() by A68, 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;
A69: (ast F1()) term v,t = nt -tree ts by Th46;
reconsider aa = (ast F1()) term v,t as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
A70: nt `1 = ast F1() by MCART_1:7;
A71: f * p = <*fv,ft*> by FINSEQ_2:40;
reconsider q = f * p as FinSequence of Union the Sorts of (Free F1(),(MSVars F1())) ;
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:9;
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:9;
then r is ArgumentSeq of Sym (ast F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by A69, 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, A69
.= F5(((f * ts) . 1),((f * ts) . 2)) by A70, FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by A71, FINSEQ_1:61 ;
hence f . ((ast F1()) term v,t) = F5((f . v),(f . t)) by A71, FINSEQ_1:61; :: thesis: verum