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 the carrier of K345(S,b₂),
for T being c-Term of , 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 the carrier of K345(S,b₁),
for T being c-Term of , st T = t holds
the_sort_of T = the_sort_of t
let V be Variables of A; :: thesis: for t being Term of the carrier of K345(S,V),
for T being c-Term of , st T = t holds
the_sort_of T = the_sort_of t
defpred S₁[ set ] means for t' being Term of the carrier of K345(S,V),
for T being c-Term of , st t' = $1 & T = t' holds
the_sort_of T = the_sort_of t';
A1: for s being SortSymbol of
for v being Element of V . s holds S₁[ root-tree [v,s]]

proof

let s be SortSymbol of ; :: 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 the carrier of K345(S,V),; :: thesis: for T being c-Term of , st t = root-tree [v,s] & T = t holds
the_sort_of T = the_sort_of t
let T be c-Term of ,; :: 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
for p being ArgumentSeq of Sym o,V st ( for t' being Term of the carrier of K345(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 ; :: thesis: for p being ArgumentSeq of Sym o,V st ( for t' being Term of the carrier of K345(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 the carrier of K345(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 the carrier of K345(S,V), st t' in rng p holds
for t being Term of the carrier of K345(S,V),
for T being c-Term of , 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 the carrier of K345(S,V),; :: thesis: for T being c-Term of , 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 ,; :: 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 the carrier of K345(S,V), holds S₁[t] from MSATERM:sch 1(A1, A4);
hence for t being Term of the carrier of K345(S,V),
for T being c-Term of , st T = t holds
the_sort_of T = the_sort_of t ; :: thesis: verum