let S be non void Signature; :: thesis: for X, Y being V5() ManySortedSet of
for t1 being Term of the carrier of (DTConMSA X),
for t2 being Term of the carrier of (DTConMSA 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 the carrier of (DTConMSA X),
for t2 being Term of the carrier of (DTConMSA Y), st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let t1 be Term of the carrier of (DTConMSA X),; :: thesis: for t2 being Term of the carrier of (DTConMSA Y), st t1 = t2 holds
the_sort_of t1 = the_sort_of t2
let t2 be Term of the carrier of (DTConMSA 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 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 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 , 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 , y being Element of Y . s' such that
A3: t2 . {} = [y,s'] by A1, A2, MSATERM:2;
t1 = root-tree [x,s] by A2, MSATERM:5;
then A4: the_sort_of t1 = s by MSATERM:14;
t2 = root-tree [y,s'] by A3, MSATERM:5;
then the_sort_of t2 = s' by MSATERM:14;
hence the_sort_of t1 = the_sort_of t2 by A1, A2, A3, A4, 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
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 by A5;
A8: z = the carrier of S by A6, TARSKI:def 1;
then the_sort_of t1 = the_result_sort_of o by A7, MSATERM:17;
hence the_sort_of t1 = the_sort_of t2 by A1, A7, A8, MSATERM:17; :: thesis: verum

end;

end;