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();
ABCMIZ_1:def 56 f .: ( the Sorts of (Free (F1(),(MSVars F1()))) . s) c= the Sorts of (Free (F1(),(MSVars F1()))) . slet x be
object ;
TARSKI:def 3 ( 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)
;
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;
S1[y -term F1()]
set a =
y -term F1();
let s be
SortSymbol of
F1();
( 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
;
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;
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();
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();
( 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]
;
S1[c -trm p]
set a =
c -trm p;
set nt =
[c, the carrier of F1()];
let s be
SortSymbol of
F1();
( 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
;
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()
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}))
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;
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();
( S1[v] implies S1[(non_op F1()) term v] )
assume A30:
S1[
v]
;
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();
( (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
;
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}))
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;
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();
( 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]
;
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();
( S1[t] implies S1[(ast F1()) term (v,t)] )
assume A39:
S1[
t]
;
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();
( (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
;
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}))
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;
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;
verum
end;
then reconsider f = f as term-transformation of F1(), MSVars F1() ;
take
f
; ( ( 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 ( ( 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();
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();
( 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
;
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}))
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;
verum
end;
hereby 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();
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}))
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;
verum
end;
let v be expression of F1(), an_Adj F1(); 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(); 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}))
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; verum