let S be non void Signature; for X, Y being non-empty 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 non-empty 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 t1 be Term of S,X; 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; ( t1 = t2 implies the_sort_of t1 = the_sort_of t2 )
assume A1:
t1 = t2
; 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]
;
the_sort_of t1 = the_sort_of t2then 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;
verum end;