let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of 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 of 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 t' being Term of S,V
for T being c-Term of A,V st t' = $1 & T = t' holds
the_sort_of T = the_sort_of t';
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 ( t = root-tree [v,s] & T = t ) ; :: thesis: the_sort_of T = the_sort_of t
then ( the_sort_of t = s & the_sort_of T = s ) by MSATERM:14, MSATERM:16;
hence the_sort_of T = the_sort_of t ; :: thesis: verum

end;

A2: for o being OperSymbol of S
for p being ArgumentSeq of Sym o,V st ( for t' being Term of S,V st t' in rng p holds
S₁[t'] ) 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 t' being Term of S,V st t' in rng p holds
S₁[t'] ) holds
S₁[[o,the carrier of S] -tree p]
let p be ArgumentSeq of Sym o,V; :: thesis: ( ( for t' being Term of S,V st t' in rng p holds
S₁[t'] ) implies S₁[[o,the carrier of S] -tree p] )
assume for t' being Term of S,V st t' in rng p holds
for t being Term of S,V
for T being c-Term of A,V st t = t' & 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 A3: 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 A3, MSATERM:17; :: thesis: verum

end;

for t being Term of S,V holds S₁[t] from MSATERM:sch 1(A1, A2);
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