let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra of 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₁[ set ] means ex t being c-Term of A,V ex vt being finite DecoratedTree st
( t = $1 & vt is_an_evaluation_of t,f );
A1: for s being SortSymbol of S
for x being Element of the Sorts of A . s holds S₁[ root-tree [x,s]]

proof

let s be SortSymbol of S; :: thesis:
let x be Element of the Sorts of A . s; :: thesis:
reconsider t = root-tree [x,s] as c-Term of A,V by Th6;
take t ; :: thesis:
take root-tree x ; :: thesis:
thus t = root-tree [x,s] ; :: thesis:
thus root-tree x is_an_evaluation_of t,f by Th31; :: thesis:

end;

A2: for s being SortSymbol of S
for v being Element of V . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of S; :: thesis:
let x be Element of V . s; :: thesis:
reconsider t = root-tree [x,s] as c-Term of A,V by Th8;
take t ; :: thesis:
take root-tree ((f . s) . x) ; :: thesis:
thus t = root-tree [x,s] ; :: thesis:
thus root-tree ((f . s) . x) is_an_evaluation_of t,f by Th32; :: thesis:

end;

A3: for o being OperSymbol of S
for p being ArgumentSeq of o,A,V st ( for t being c-Term of A,V st t in rng p holds
S₁[t] ) holds
S₁[(Sym o,(the Sorts of A \/ V)) -tree p]

proof

let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of o,A,V; :: thesis:
assume A4: for t being c-Term of A,V st t in rng p holds
ex u being c-Term of A,V ex vt being finite DecoratedTree st
( u = t & vt is_an_evaluation_of u,f ) ; :: thesis:
A5: dom p = Seg (len p) by FINSEQ_1:def 3;
defpred S₂[ set , set ] means ex t being c-Term of A,V ex vt being finite DecoratedTree st
( $2 = vt & t = p . $1 & vt is_an_evaluation_of t,f );
A6: for e being set st e in dom p holds
ex u being set st S₂[e,u]

proof

let x be set ; :: thesis:
assume x in dom p ; :: thesis:
then A7: ( p . x in rng p & rng p c= S -Terms (the Sorts of A \/ V) ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider t = p . x as c-Term of A,V ;
ex u being c-Term of A,V ex vt being finite DecoratedTree st
( u = t & vt is_an_evaluation_of u,f ) by A4, A7;
hence ex u being set st S₂[x,u] ; :: thesis:

end;

consider q being Function such that
A8: ( dom q = dom p & ( for x being set st x in dom p holds
S₂[x,q . x] ) ) from CLASSES1:sch 1(A6);
reconsider q = q as FinSequence by A5, A8, FINSEQ_1:def 2;
A9: len p = len q by A8, FINSEQ_3:31;

now

let x be set ; :: thesis:
assume x in dom q ; :: thesis:
then ex t being c-Term of A,V ex vt being finite DecoratedTree st
( q . x = vt & t = p . x & vt is_an_evaluation_of t,f ) by A8;
hence q . x is DecoratedTree ; :: thesis:

end;

then reconsider q = q as DTree-yielding FinSequence by TREES_3:26;

now

let i be Nat; :: thesis:
let t be c-Term of A,V; :: thesis:
assume i in dom p ; :: thesis:
then ex t being c-Term of A,V ex vt being finite DecoratedTree st
( q . i = vt & t = p . i & vt is_an_evaluation_of t,f ) by A8;
hence ( t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) ; :: thesis:

end;

then ex vt being finite DecoratedTree st
( vt = ((Den o,A) . (roots q)) -tree q & vt is_an_evaluation_of (Sym o,(the Sorts of A \/ V)) -tree p,f ) by A9, Th33;
hence S₁[(Sym o,(the Sorts of A \/ V)) -tree p] ; :: thesis:

end;

for t being c-Term of A,V holds S₁[t] from MSATERM:sch 2(A1, A2, A3);
then ex u being c-Term of A,V ex vt being finite DecoratedTree st
( u = t & vt is_an_evaluation_of u,f ) ;
hence ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f ; :: thesis: