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:
let s be SortSymbol of S; :: thesis:
let x be Element of the Sorts of A . s; :: thesis:
assume A1: t = root-tree [x,s] ; :: thesis:
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:
let p be Node of (root-tree x); :: thesis:
reconsider e = p as empty FinSequence of NAT by A3, TARSKI:def 1, TREES_1:29;

hereby :: thesis:

let s1 be SortSymbol of S; :: thesis:
let v be Element of V . s1; :: thesis:
assume t . p = [v,s1] ; :: thesis:
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:

end;

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

hereby :: thesis:

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

end;

let o be OperSymbol of S; :: thesis:
assume t . p = [o, the carrier of S] ; :: thesis:
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: