let S be non void Signature; :: thesis: for X, Y being V8() ManySortedSet of the carrier of S
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 V8() ManySortedSet of the carrier of S; :: 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:
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:
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:87;
then consider s9 being SortSymbol of S, y being Element of Y . s9 such that
A3: t2 . {} = [y,s9] by ;
t1 = root-tree [x,s] by ;
then A4: the_sort_of t1 = s by MSATERM:14;
t2 = root-tree [y,s9] by ;
then the_sort_of t2 = s9 by MSATERM:14;
hence the_sort_of t1 = the_sort_of t2 by ; :: thesis: verum
end;
suppose t1 . {} in [: the carrier' of S,{ the carrier of S}:] ; :: thesis:
then consider o, z being object such that
A5: o in the carrier' of S and
A6: z in { the carrier of S} and
A7: t1 . {} = [o,z] by ZFMISC_1:def 2;
reconsider o = o as OperSymbol of S by A5;
A8: z = the carrier of S by ;
then the_sort_of t1 = the_result_sort_of o by ;
hence the_sort_of t1 = the_sort_of t2 by ; :: thesis: verum
end;
end;