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 Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
let A be non-empty MSAlgebra over S; :: thesis: for V being Variables of A
for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
let V be Variables of A; :: thesis: for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t
defpred S₁[ set ] means for t9 being Term of S,V
for T being c-Term of A,V st t9 = $1 & T = t9 holds
the_sort_of T = the_sort_of t9;
A1: 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 v be Element of V . s; :: thesis: S₁[ root-tree [v,s]]
let t be Term of S,V; :: thesis: for T being c-Term of A,V st t = root-tree [v,s] & T = t holds
the_sort_of T = the_sort_of t
let T be c-Term of A,V; :: thesis: ( t = root-tree [v,s] & T = t implies the_sort_of T = the_sort_of t )
assume that
A2: t = root-tree [v,s] and
A3: T = t ; :: thesis: the_sort_of T = the_sort_of t
the_sort_of t = s by A2, MSATERM:14;
hence the_sort_of T = the_sort_of t by A2, A3, MSATERM:16; :: thesis: verum

end;

A4: for o being OperSymbol of S
for p being ArgumentSeq of Sym (o,V) st ( for t9 being Term of S,V st t9 in rng p holds
S₁[t9] ) holds
S₁[[o, the carrier of S] -tree p]

proof

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,V) st ( for t9 being Term of S,V st t9 in rng p holds
S₁[t9] ) holds
S₁[[o, the carrier of S] -tree p]
let p be ArgumentSeq of Sym (o,V); :: thesis: ( ( for t9 being Term of S,V st t9 in rng p holds
S₁[t9] ) implies S₁[[o, the carrier of S] -tree p] )
assume for t9 being Term of S,V st t9 in rng p holds
for t being Term of S,V
for T being c-Term of A,V st t = t9 & T = t holds
the_sort_of T = the_sort_of t ; :: thesis: S₁[[o, the carrier of S] -tree p]
let t be Term of S,V; :: thesis: for T being c-Term of A,V st t = [o, the carrier of S] -tree p & T = t holds
the_sort_of T = the_sort_of t
let T be c-Term of A,V; :: thesis: ( t = [o, the carrier of S] -tree p & T = t implies the_sort_of T = the_sort_of t )
assume t = [o, the carrier of S] -tree p ; :: thesis: ( not T = t or the_sort_of T = the_sort_of t )
then A5: t . {} = [o, the carrier of S] by TREES_4:def 4;
then the_sort_of t = the_result_sort_of o by MSATERM:17;
hence ( not T = t or the_sort_of T = the_sort_of t ) by A5, MSATERM:17; :: thesis: verum

end;

for t being Term of S,V holds S₁[t] from MSATERM:sch 1(A1, A4);
hence for t being Term of S,V
for T being c-Term of A,V st T = t holds
the_sort_of T = the_sort_of t ; :: thesis: verum