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

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 ((f . s) . x)) . p = x ) & ( for o being OperSymbol of S st t . p = [o, the carrier of S] holds
(root-tree ((f . s) . x)) . p = (Den (o,A)) . (succ ((root-tree ((f . s) . x)),p)) ) )

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

end;

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

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

end;

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