let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S
for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let A be non-empty MSAlgebra over S; :: thesis: for V being Variables of A
for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let V be Variables of A; :: thesis: for t being c-Term of A,V
for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let t be c-Term of A,V; :: thesis: for f being ManySortedFunction of V, the Sorts of A ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
let f be ManySortedFunction of V, the Sorts of A; :: thesis: ex vt being finite DecoratedTree st vt is_an_evaluation_of t,f
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 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: 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]
let p be ArgumentSeq of o,A,V; :: thesis: ( ( for t being c-Term of A,V st t in rng p holds
S₁[t] ) implies S₁[(Sym (o,( the Sorts of A (\/) V))) -tree p] )
assume A2: 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: S₁[(Sym (o,( the Sorts of A (\/) V))) -tree p]
defpred S₂[ object , object ] 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 );
A3: for e being object st e in dom p holds
ex u being object st S₂[e,u]

proof

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

end;

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

now :: thesis: for x being object st x in dom q holds
q . x is DecoratedTree

let x be object ; :: thesis: ( x in dom q implies q . x is DecoratedTree )
assume x in dom q ; :: thesis: q . x is DecoratedTree
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 A5;
hence q . x is DecoratedTree ; :: thesis: verum

end;

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

now :: thesis: 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 )

let i be Nat; :: thesis: 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 )
let t be c-Term of A,V; :: thesis: ( i in dom p & t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) )
assume i in dom p ; :: thesis: ( t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) )
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 A5;
hence ( t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) ; :: thesis: verum

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 A6, Th33;
hence S₁[(Sym (o,( the Sorts of A (\/) V))) -tree p] ; :: thesis: verum

end;

A7: 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: for v being Element of V . s holds S₁[ root-tree [v,s]]
let x be Element of V . s; :: thesis: S₁[ root-tree [x,s]]
reconsider t = root-tree [x,s] as c-Term of A,V by Th8;
take t ; :: thesis: ex vt being finite DecoratedTree st
( t = root-tree [x,s] & vt is_an_evaluation_of t,f )
take root-tree ((f . s) . x) ; :: thesis: ( t = root-tree [x,s] & root-tree ((f . s) . x) is_an_evaluation_of t,f )
thus t = root-tree [x,s] ; :: thesis: root-tree ((f . s) . x) is_an_evaluation_of t,f
thus root-tree ((f . s) . x) is_an_evaluation_of t,f by Th32; :: thesis: verum

end;

A8: 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: for x being Element of the Sorts of A . s holds S₁[ root-tree [x,s]]
let x be Element of the Sorts of A . s; :: thesis: S₁[ root-tree [x,s]]
reconsider t = root-tree [x,s] as c-Term of A,V by Th6;
take t ; :: thesis: ex vt being finite DecoratedTree st
( t = root-tree [x,s] & vt is_an_evaluation_of t,f )
take root-tree x ; :: thesis: ( t = root-tree [x,s] & root-tree x is_an_evaluation_of t,f )
thus t = root-tree [x,s] ; :: thesis: root-tree x is_an_evaluation_of t,f
thus root-tree x is_an_evaluation_of t,f by Th31; :: thesis: verum

end;

for t being c-Term of A,V holds S₁[t] from MSATERM:sch 2(A8, A7, A1);
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: verum