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 object ; :: 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) ;
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 ;
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: c <> * by Def11;
A20: c <> non_op by Def11;
A21: 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 A22: rng p c= dom f ;
rng (f * p) c= QuasiTerms F1()
proof
let z be object ; :: 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 object such that
A23: i in dom (f * p) and
A24: z = (f * p) . i by FUNCT_1:def 3;
i in dom p by A22, A23, RELAT_1:27;
then A25: p . i in rng p by FUNCT_1:def 3;
then reconsider pi1 = p . i as quasi-term of F1() by A21, 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, A25;
hence z in QuasiTerms F1() by A23, A24, 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 object ; :: 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;
A26: len q = len p by A22, FINSEQ_2:29;
c -trm p is Term of F1(),((MSVars F1()) (\/) ( the carrier of F1() --> {0})) by MSAFREE3:8;
then A27: r is ArgumentSeq of Sym (c,((MSVars F1()) (\/) ( the carrier of F1() --> {0}))) by A17, MSATERM:1;
then A28: the_result_sort_of c = s by A17, A18, MSATERM:20;
Sym (c,((MSVars F1()) (\/) ( the carrier of F1() --> {0}))) ==> roots r by A27, 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, FUNCOP_1:def 8
.= F4(c,(f * ts)) by A20, FUNCOP_1:def 8 ;
then f . (c -trm p) is expression of F1(), the_result_sort_of c by A2, A14, A26;
hence f . (c -trm p) in the Sorts of (Free (F1(),(MSVars F1()))) . s by A28, Def28; :: thesis: verum
end;
A29: 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 A30: S1[v] ; :: thesis: S1[(non_op F1()) term v]
A31: 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 A30;
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 A32: (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
A33: (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 A32, Def28;
then A34: s = an_Adj F1() by A33, 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 A31, 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;
A35: (non_op F1()) term v = nt -tree ts by Th43;
dom f = Union the Sorts of (Free (F1(),(MSVars F1()))) by FUNCT_2:def 1;
then A36: f * p = <*fv*> by FINSEQ_2:34;
rng p c= F1() -Terms ((MSVars F1()) (\/) ( the carrier of F1() --> {0}))
proof
let z be object ; :: 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 A35, 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, A35
.= IFEQ ((non_op F1()),non_op,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts))) by FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8
.= F3(fv) by A36, 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 A34, Def28; :: thesis: verum
end;
A37: 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 A38: 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 A39: S1[t] ; :: thesis: S1[(ast F1()) term (v,t)]
A40: v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Def28;
A41: t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by Def28;
A42: f . v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A38, A40;
A43: f . t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by A39, A41;
reconsider fv = f . v as expression of F1(), an_Adj F1() by A42, Def28;
reconsider ft = f . t as expression of F1(), a_Type F1() by A43, 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 A44: (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
A45: (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 A44, Def28;
then A46: s = a_Type F1() by A45, 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;
A47: (ast F1()) term (v,t) = nt -tree ts by Th46;
A48: f * p = <*fv,ft*> by FINSEQ_2:36;
rng p c= F1() -Terms ((MSVars F1()) (\/) ( the carrier of F1() --> {0}))
proof
let z be object ; :: 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 A47, 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, A47
.= F5(((f * ts) . 1),((f * ts) . 2)) by FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by A48, FINSEQ_1:44
.= F5(fv,ft) by A48, 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 A46, Def28; :: thesis: verum
end;
S1[a] from ABCMIZ_1:sch 2(A9, A13, A29, A37);
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 A49: 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 A49, MSAFREE3:2;
xx in Terminals (DTConMSA (MSVars F1())) by A49, MSAFREE:7;
hence f . (x -term F1()) = F2((xx `1)) by A5
.= F2(x) ;
:: 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
A50: len p = len (the_arity_of c) and
A51: 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;
A52: c -trm p = nt -tree ts by A50, Def35;
A53: c <> * by Def11;
A54: c <> non_op by Def11;
rng p c= F1() -Terms ((MSVars F1()) (\/) ( the carrier of F1() --> {0}))
proof
let z be object ; :: 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 A52, 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, A52
.= IFEQ (c,non_op,F3(((f * ts) . 1)),F4(c,(f * ts))) by A53, FUNCOP_1:def 8
.= F4(c,(f * ts)) by A54, FUNCOP_1:def 8 ;
hence f . (c -trm p) = F4(c,q) by A51; :: 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))
A55: 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 A55, 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;
A56: (non_op F1()) term v = nt -tree ts by Th43;
dom f = Union the Sorts of (Free (F1(),(MSVars F1()))) by FUNCT_2:def 1;
then A57: f * p = <*fv*> by FINSEQ_2:34;
rng p c= F1() -Terms ((MSVars F1()) (\/) ( the carrier of F1() --> {0}))
proof
let z be object ; :: 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 A56, 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, A56
.= IFEQ ((non_op F1()),non_op,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts))) by FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8 ;
hence f . ((non_op F1()) term v) = F3((f . v)) by A57, 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))
A58: v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by Def28;
A59: t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by Def28;
A60: f . v in the Sorts of (Free (F1(),(MSVars F1()))) . (an_Adj F1()) by A58, Th129;
A61: f . t in the Sorts of (Free (F1(),(MSVars F1()))) . (a_Type F1()) by A59, Th129;
reconsider fv = f . v as expression of F1(), an_Adj F1() by A60, Def28;
reconsider ft = f . t as expression of F1(), a_Type F1() by A61, 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;
A62: (ast F1()) term (v,t) = nt -tree ts by Th46;
A63: f * p = <*fv,ft*> by FINSEQ_2:36;
rng p c= F1() -Terms ((MSVars F1()) (\/) ( the carrier of F1() --> {0}))
proof
let z be object ; :: 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 A62, 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, A62
.= F5(((f * ts) . 1),((f * ts) . 2)) by FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by A63, FINSEQ_1:44 ;
hence f . ((ast F1()) term (v,t)) = F5((f . v),(f . t)) by A63, FINSEQ_1:44; :: thesis: verum