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
A6: for t being Symbol of (DTConMSA (MSVars F1())) st t in Terminals (DTConMSA (MSVars F1())) holds
f . (root-tree t) = H2(t) and
A7: 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();
 A5: Union the Sorts of (Free F1(),(MSVars F1())) = TS (DTConMSA (MSVars F1())) by LemTS;
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
B1: ( a in the Sorts of (Free F1(),(MSVars F1())) . s & 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;
W1: 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 C1: 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
C2: [y,(a_Term F1())] in Terminals (DTConMSA (MSVars F1())) by LemTerm;
then reconsider t = [y,(a_Term F1())] as Symbol of (DTConMSA (MSVars F1())) ;
f . (y -term F1()) = H2(t) by A6, C2
.= F2(y) by MCART_1:7 ;
then C3: ( f . (y -term F1()) is quasi-term of F1() & y -term F1() is expression of F1(),s ) by A1, C1, ELEMENT;
then s = a_Term F1() by Th90A;
hence f . (y -term F1()) in the Sorts of (Free F1(),(MSVars F1())) . s by C3, ELEMENT; :: thesis: verum
end;
W2: 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
Z0: len p = len (the_arity_of c) and
Z1: 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 00: 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 LemNTerm;
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 A5;
Z3: c -trm p = nt -tree ts by Z0, TERM;
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 00;
then aa in FreeSort ((MSVars F1()) \/ (the carrier of F1() --> {0 })),s by MSAFREE:def 13;
then 01: the_sort_of aa = s by MSATERM:def 5;
Z4: ( nt `1 = c & c <> * & c <> non_op ) by CNSTR2, MCART_1:7;
Z5: 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 Z7: 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
V1: ( i in dom (f * p) & z = (f * p) . i ) by FUNCT_1:def 5;
i in dom p by V1, Z7, RELAT_1:46;
then V2: p . i in rng p by FUNCT_1:def 5;
then reconsider pi = p . i as quasi-term of F1() by Z5, Th42;
( pi in the Sorts of (Free F1(),(MSVars F1())) . (a_Term F1()) & S1[pi] ) by Z1, V2, Th42;
then f . pi in the Sorts of (Free F1(),(MSVars F1())) . (a_Term F1()) ;
hence z in QuasiTerms F1() by V1, 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;
Z6: len q = len p by Z7, FINSEQ_2:33;
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 Z3, MSATERM:1;
then 02: ( the_result_sort_of c = s & Sym c,((MSVars F1()) \/ (the carrier of F1() --> {0 })) ==> roots r ) by 01, Z3, MSATERM:20, MSATERM:21;
then nt ==> roots ts by LemArr;
then f . (c -trm p) = H3(nt, roots ts,f * ts) by A7, Z3
.= IFEQ c,non_op ,F3(((f * ts) . 1)),F4(c,(f * ts)) by Z4, FUNCOP_1:def 8
.= F4(c,(f * ts)) by Z4, FUNCOP_1:def 8 ;
then f . (c -trm p) is expression of F1(), the_result_sort_of c by Z0, Z6, A2;
hence f . (c -trm p) in the Sorts of (Free F1(),(MSVars F1())) . s by 02, ELEMENT; :: thesis: verum
end;
W3: 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 Z1: S1[v] ; :: thesis: S1[(non_op F1()) term v]
Y1: v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by ELEMENT;
then Y2: f . v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by Z1;
then reconsider fv = f . v as expression of F1(), an_Adj F1() by ELEMENT;
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 00: (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
then ( (non_op F1()) term v is expression of F1(), an_Adj F1() & (non_op F1()) term v is expression of F1(),s ) by ELEMENT, ThNon;
then 03: s = an_Adj F1() by Th90A;
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 Y1, 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 LemNTerm;
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 A5;
Z3: (non_op F1()) term v = nt -tree ts by ThNon;
reconsider aa = (non_op F1()) term v 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 00;
then aa in FreeSort ((MSVars F1()) \/ (the carrier of F1() --> {0 })),s by MSAFREE:def 13;
then 01: the_sort_of aa = s by MSATERM:def 5;
Z4: ( nt `1 = non_op F1() & non_op F1() <> * ) by MCART_1:7;
dom f = Union the Sorts of (Free F1(),(MSVars F1())) by FUNCT_2:def 1;
then 08: 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 Y2, ZFMISC_1:37;
then reconsider q = f * p as FinSequence of the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by 08, 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 Th42;
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 Z3, MSATERM:1;
then ( the_result_sort_of (non_op F1()) = s & Sym (non_op F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) ==> roots r ) by 01, Z3, MSATERM:20, MSATERM:21;
then nt ==> roots ts by LemArr;
then f . ((non_op F1()) term v) = H3(nt, roots ts,f * ts) by A7, Z3
.= IFEQ (non_op F1()),non_op ,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts)) by Z4, FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8
.= F3(fv) by 08, 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 03, ELEMENT; :: thesis: verum
end;
W4: 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 Z0: 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 Z1: S1[t] ; :: thesis: S1[(ast F1()) term v,t]
( v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) & t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) ) by ELEMENT;
then Y2: ( f . v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) & f . t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) ) by Z0, Z1;
then reconsider fv = f . v as expression of F1(), an_Adj F1() by ELEMENT;
reconsider ft = f . t as expression of F1(), a_Type F1() by Y2, ELEMENT;
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 00: (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
then ( (ast F1()) term v,t is expression of F1(), a_Type F1() & (ast F1()) term v,t is expression of F1(),s ) by ELEMENT, ThAst;
then 03: s = a_Type F1() by Th90A;
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 LemNTerm;
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 A5;
Z3: (ast F1()) term v,t = nt -tree ts by ThAst;
reconsider aa = (ast F1()) term v,t 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 00;
then aa in FreeSort ((MSVars F1()) \/ (the carrier of F1() --> {0 })),s by MSAFREE:def 13;
then 01: the_sort_of aa = s by MSATERM:def 5;
Z4: ( nt `1 = ast F1() & ast F1() <> non_op ) by MCART_1:7;
08: 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 Z3, MSATERM:1;
then ( the_result_sort_of (ast F1()) = s & Sym (ast F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) ==> roots r ) by 01, Z3, MSATERM:20, MSATERM:21;
then nt ==> roots ts by LemArr;
then f . ((ast F1()) term v,t) = H3(nt, roots ts,f * ts) by A7, Z3
.= F5(((f * ts) . 1),((f * ts) . 2)) by Z4, FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by 08, FINSEQ_1:61
.= F5(fv,ft) by 08, 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 03, ELEMENT; :: thesis: verum
end;
S1[a] from ABCMIZ_1:sch 2(W1, W2, W3, W4);
 hence x in the Sorts of (Free F1(),(MSVars F1())) . s by B1; :: 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 00: x in (MSVars F1()) . (a_Term F1()) by MSVARS;
then reconsider x' = x as Element of (MSVars F1()) . (a_Term F1()) ;
reconsider xx = [x',(a_Term F1())] as Symbol of (DTConMSA (MSVars F1())) by 00, MSAFREE3:3;
( x -term F1() = root-tree xx & xx in Terminals (DTConMSA (MSVars F1())) ) by 00, MSAFREE:7;
hence f . (x -term F1()) = F2((xx `1 )) by A6
.= 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 Z0: ( len p = len (the_arity_of c) & 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 LemNTerm;
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 A5;
Z3: c -trm p = nt -tree ts by Z0, TERM;
reconsider aa = c -trm p as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
Z4: ( nt `1 = c & c <> * & c <> non_op ) by CNSTR2, MCART_1:7;
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 Z3, MSATERM:1;
then Sym c,((MSVars F1()) \/ (the carrier of F1() --> {0 })) ==> roots r by MSATERM:21;
then nt ==> roots ts by LemArr;
then f . (c -trm p) = H3(nt, roots ts,f * ts) by A7, Z3
.= IFEQ c,non_op ,F3(((f * ts) . 1)),F4(c,(f * ts)) by Z4, FUNCOP_1:def 8
.= F4(c,(f * ts)) by Z4, FUNCOP_1:def 8 ;
hence f . (c -trm p) = F4(c,q) by Z0; :: 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))
Y1: v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by ELEMENT;
then Y2: f . v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by ThTr;
then reconsider fv = f . v as expression of F1(), an_Adj F1() by ELEMENT;
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 Y1, 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 LemNTerm;
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 A5;
Z3: (non_op F1()) term v = nt -tree ts by ThNon;
reconsider aa = (non_op F1()) term v as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
Z4: ( nt `1 = non_op F1() & non_op F1() <> * ) by MCART_1:7;
dom f = Union the Sorts of (Free F1(),(MSVars F1())) by FUNCT_2:def 1;
then 08: 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 Y2, ZFMISC_1:37;
then reconsider q = f * p as FinSequence of the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) by 08, 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 Th42;
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 Z3, MSATERM:1;
then Sym (non_op F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) ==> roots r by MSATERM:21;
then nt ==> roots ts by LemArr;
then f . ((non_op F1()) term v) = H3(nt, roots ts,f * ts) by A7, Z3
.= IFEQ (non_op F1()),non_op ,F3(((f * ts) . 1)),F4((non_op F1()),(f * ts)) by Z4, FUNCOP_1:def 8
.= F3(((f * ts) . 1)) by FUNCOP_1:def 8 ;
hence f . ((non_op F1()) term v) = F3((f . v)) by 08, 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))
( v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) & t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) ) by ELEMENT;
then Y2: ( f . v in the Sorts of (Free F1(),(MSVars F1())) . (an_Adj F1()) & f . t in the Sorts of (Free F1(),(MSVars F1())) . (a_Type F1()) ) by ThTr;
then reconsider fv = f . v as expression of F1(), an_Adj F1() by ELEMENT;
reconsider ft = f . t as expression of F1(), a_Type F1() by Y2, ELEMENT;
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 LemNTerm;
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 A5;
Z3: (ast F1()) term v,t = nt -tree ts by ThAst;
reconsider aa = (ast F1()) term v,t as Term of F1(),((MSVars F1()) \/ (the carrier of F1() --> {0 })) by MSAFREE3:9;
Z4: ( nt `1 = ast F1() & ast F1() <> non_op ) by MCART_1:7;
08: 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 Z3, MSATERM:1;
then Sym (ast F1()),((MSVars F1()) \/ (the carrier of F1() --> {0 })) ==> roots r by MSATERM:21;
then nt ==> roots ts by LemArr;
then f . ((ast F1()) term v,t) = H3(nt, roots ts,f * ts) by A7, Z3
.= F5(((f * ts) . 1),((f * ts) . 2)) by Z4, FUNCOP_1:def 8
.= F5(fv,((f * ts) . 2)) by 08, FINSEQ_1:61 ;
hence f . ((ast F1()) term v,t) = F5((f . v),(f . t)) by 08, FINSEQ_1:61; :: thesis: verum