let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra over S; :: thesis:
let V be Variables of A; :: thesis:
let t be c-Term of A,V; :: thesis:
let f be ManySortedFunction of V, the Sorts of A; :: thesis:
defpred S₁[ c-Term of A,V] means for vt being finite DecoratedTree st vt is_an_evaluation_of $1,f holds
vt . {} in the Sorts of A . (the_sort_of $1);

A1: now :: thesis:

let s be SortSymbol of S; :: thesis:
let v be Element of V . s; :: thesis:
thus S₁[v -term A] :: thesis:

proof

let vt be finite DecoratedTree; :: thesis:
set t = v -term A;
assume A2: vt is_an_evaluation_of v -term A,f ; :: thesis:
root-tree ((f . s) . v) is_an_evaluation_of v -term A,f by Th32;
then vt = root-tree ((f . s) . v) by A2, Th37;
then A3: vt . {} = (f . s) . v by TREES_4:3;
s = the_sort_of (v -term A) by Th19;
hence vt . {} in the Sorts of A . (the_sort_of (v -term A)) by A3; :: thesis:

end;

end;

A4: now :: thesis:

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of o,A,V; :: thesis:
assume A5: for t being c-Term of A,V st t in rng p holds
S₁[t] ; :: thesis:
thus S₁[(Sym (o,( the Sorts of A (\/) V))) -tree p] :: thesis:

proof

let vt be finite DecoratedTree; :: thesis:
set t = (Sym (o,( the Sorts of A (\/) V))) -tree p;
A6: dom ( the Sorts of A * the ResultSort of S) = the carrier' of S by PARTFUN1:def 2;
assume vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f ; :: thesis:
then consider q being DTree-yielding FinSequence such that
A7: len q = len p and
A8: vt = ((Den (o,A)) . (roots q)) -tree q and
A9: for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) by Th35;
A10: vt . {} = (Den (o,A)) . (roots q) by A8, TREES_4:def 4;

now :: thesis:

A11: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
A12: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
A13: dom (roots q) = dom q by TREES_3:def 18;
hence A14: dom (roots q) = Seg (len q) by FINSEQ_1:def 3
.= Seg (len (the_arity_of o)) by A7, Lm8
.= dom (the_arity_of o) by FINSEQ_1:def 3
.= dom ( the Sorts of A * (the_arity_of o)) by A12, A11, RELAT_1:27 ;
:: thesis:
let x be object ; :: thesis:
assume A15: x in dom ( the Sorts of A * (the_arity_of o)) ; :: thesis:
then consider i being Element of NAT such that
A16: x = i + 1 and
A17: i < len q by A13, A14, Lm1;
A18: ex T being DecoratedTree st
( T = q . (i + 1) & (roots q) . (i + 1) = T . {} ) by A13, A14, A15, A16, TREES_3:def 18;
i + 1 in dom p by A7, A17, Lm9;
then A19: ex t being c-Term of A,V st
( t = p . (i + 1) & t = p /. (i + 1) & the_sort_of t = (the_arity_of o) . (i + 1) & the_sort_of t = (the_arity_of o) /. (i + 1) ) by Lm8;
reconsider t = p . (i + 1) as c-Term of A,V by A7, A17, Lm2;
consider vt being finite DecoratedTree such that
A20: vt = q . (i + 1) and
A21: vt is_an_evaluation_of t,f by A7, A9, A17, Lm9;
vt . {} in the Sorts of A . (the_sort_of t) by A5, A7, A17, A21, Lm9;
hence (roots q) . x in ( the Sorts of A * (the_arity_of o)) . x by A15, A16, A18, A20, A19, FUNCT_1:12; :: thesis:

end;

then roots q in product ( the Sorts of A * (the_arity_of o)) by CARD_3:9;
then roots q in ( the Sorts of A #) . (the_arity_of o) by FINSEQ_2:def 5;
then A22: roots q in ( the Sorts of A #) . ( the Arity of S . o) by MSUALG_1:def 1;
dom (( the Sorts of A #) * the Arity of S) = the carrier' of S by PARTFUN1:def 2;
then roots q in (( the Sorts of A #) * the Arity of S) . o by A22, FUNCT_1:12;
then A23: roots q in Args (o,A) by MSUALG_1:def 4;
Result (o,A) = ( the Sorts of A * the ResultSort of S) . o by MSUALG_1:def 5
.= the Sorts of A . ( the ResultSort of S . o) by A6, FUNCT_1:12
.= the Sorts of A . (the_result_sort_of o) by MSUALG_1:def 2
.= the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A (\/) V))) -tree p)) by Th20 ;
hence vt . {} in the Sorts of A . (the_sort_of ((Sym (o,( the Sorts of A (\/) V))) -tree p)) by A10, A23, FUNCT_2:5; :: thesis:

end;

end;

A24: now :: thesis:

let s be SortSymbol of S; :: thesis:
let x be Element of the Sorts of A . s; :: thesis:
thus S₁[x -term (A,V)] :: thesis:

proof

let vt be finite DecoratedTree; :: thesis:
set t = x -term (A,V);
assume A25: vt is_an_evaluation_of x -term (A,V),f ; :: thesis:
root-tree x is_an_evaluation_of x -term (A,V),f by Th31;
then vt = root-tree x by A25, Th37;
then A26: vt . {} = x by TREES_4:3;
s = the_sort_of (x -term (A,V)) by Th15;
hence vt . {} in the Sorts of A . (the_sort_of (x -term (A,V))) by A26; :: thesis:

end;

end;

for t being c-Term of A,V holds S₁[t] from MSATERM:sch 3(A24, A1, A4);
hence for vt being finite DecoratedTree st vt is_an_evaluation_of t,f holds
vt . {} in the Sorts of A . (the_sort_of t) ; :: thesis: