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
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x 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
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x 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
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x 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
for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let f be ManySortedFunction of V, the Sorts of A; :: thesis: for s being SortSymbol of S
for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let s be SortSymbol of S; :: thesis: for x being Element of the Sorts of A . s st t = root-tree [x,s] holds
root-tree x is_an_evaluation_of t,f
let x be Element of the Sorts of A . s; :: thesis: ( t = root-tree [x,s] implies root-tree x is_an_evaluation_of t,f )
assume A1: t = root-tree [x,s] ; :: thesis: root-tree x is_an_evaluation_of t,f
A2: t . {} = [x,s] by A1, TREES_4:3;
set vt = root-tree x;
A3: dom (root-tree x) = elementary_tree 0 by TREES_4:3;
hence dom (root-tree x) = dom t by A1, TREES_4:3; :: according to MSATERM:def 9 :: thesis: for p being Node of (root-tree x) holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
(root-tree x) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) )
let p be Node of (root-tree x); :: thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
(root-tree x) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) )
reconsider e = p as empty FinSequence of NAT by A3, TARSKI:def 1, TREES_1:29;

hereby :: thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
(root-tree x) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) ) )

let s1 be SortSymbol of S; :: thesis: for v being Element of V . s1 st t . p = [v,s1] holds
(root-tree x) . p = (f . s1) . v
let v be Element of V . s1; :: thesis: ( t . p = [v,s1] implies (root-tree x) . p = (f . s1) . v )
assume t . p = [v,s1] ; :: thesis: (root-tree x) . p = (f . s1) . v
then A4: [v,s1] = t . e
.= [x,s] by A1, TREES_4:3 ;
then A5: x = v by XTUPLE_0:1;
s = s1 by A4, XTUPLE_0:1;
hence (root-tree x) . p = (f . s1) . v by A5, Th30; :: thesis: verum

end;

A6: (root-tree x) . {} = x by TREES_4:3;

hereby :: thesis: for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p))

let s1 be SortSymbol of S; :: thesis: for x1 being Element of the Sorts of A . s1 st t . p = [x1,s1] holds
(root-tree x) . p = x1
let x1 be Element of the Sorts of A . s1; :: thesis: ( t . p = [x1,s1] implies (root-tree x) . p = x1 )
assume t . p = [x1,s1] ; :: thesis: (root-tree x) . p = x1
then [x1,s1] = t . e ;
hence (root-tree x) . p = x1 by A2, A6, XTUPLE_0:1; :: thesis: verum

end;

let o be OperSymbol of S; :: thesis: ( t . p = [o, the carrier of S] implies (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) )
assume t . p = [o, the carrier of S] ; :: thesis: (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p))
then the carrier of S = (t . e) `2
.= s by A2 ;
hence (root-tree x) . p = (Den (o,A)) . (succ ((root-tree x),p)) by Lm7; :: thesis: verum