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: the_sort_of t1 = the_sort_of t2

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: 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;

end;

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:87;

then consider s9 being SortSymbol of S, y being Element of Y . s9 such that

A3: t2 . {} = [y,s9] 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,s9] by A3, MSATERM:5;

then the_sort_of t2 = s9 by MSATERM:14;

hence the_sort_of t1 = the_sort_of t2 by A1, A2, A3, A4, XTUPLE_0:1; :: thesis: verum

end;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 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,s9] by A3, MSATERM:5;

then the_sort_of t2 = s9 by MSATERM:14;

hence the_sort_of t1 = the_sort_of t2 by A1, A2, A3, A4, XTUPLE_0:1; :: thesis: verum

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 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 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;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 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