let S be non void Signature; :: thesis: for X, Y being V5() ManySortedSet of
for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let X, Y be V5() ManySortedSet of ; :: thesis: for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let t1 be Term of S,X; :: thesis: for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let t2 be Term of S,Y; :: thesis: ( t1 = t2 implies the_sort_of t1 = the_sort_of t2 )
assume A1: t1 = t2 ; :: thesis: the_sort_of t1 = the_sort_of t2

per cases ( ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] or t1 . {} in [:the carrier' of S,{the carrier of S}:] ) by MSATERM:2;

suppose ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] ; :: thesis: the_sort_of t1 = the_sort_of t2

then consider s being SortSymbol of S, x being Element of X . s such that
A2: t1 . {} = [x,s] ;
s in the carrier of S ;
then s <> the carrier of S ;
then not s in {the carrier of S} by TARSKI:def 1;
then not [x,s] in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:106;
then consider s' being SortSymbol of S, y being Element of Y . s' such that
A3: t2 . {} = [y,s'] by A1, A2, MSATERM:2;
( t1 = root-tree [x,s] & t2 = root-tree [y,s'] ) by A2, A3, MSATERM:5;
then ( the_sort_of t1 = s & the_sort_of t2 = s' ) by MSATERM:14;
hence the_sort_of t1 = the_sort_of t2 by A1, A2, A3, ZFMISC_1:33; :: thesis: verum

end;

suppose t1 . {} in [:the carrier' of S,{the carrier of S}:] ; :: thesis: the_sort_of t1 = the_sort_of t2

then consider o, z being set such that
A4: ( o in the carrier' of S & z in {the carrier of S} & t1 . {} = [o,z] ) by ZFMISC_1:def 2;
reconsider o = o as OperSymbol of S by A4;
z = the carrier of S by A4, TARSKI:def 1;
then ( the_sort_of t1 = the_result_sort_of o & the_sort_of t2 = the_result_sort_of o ) by A1, A4, MSATERM:17;
hence the_sort_of t1 = the_sort_of t2 ; :: thesis: verum

end;

end;