let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for t being Element of (Free (S,X))
for u being Term of S,X st t = u holds
the_sort_of t = the_sort_of u
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for t being Element of (Free (S,X))
for u being Term of S,X st t = u holds
the_sort_of t = the_sort_of u
let t be Element of (Free (S,X)); :: thesis: for u being Term of S,X st t = u holds
the_sort_of t = the_sort_of u
let u be Term of S,X; :: thesis: ( t = u implies the_sort_of t = the_sort_of u )
assume t = u ; :: thesis: the_sort_of t = the_sort_of u
then t in FreeSort (X,(the_sort_of u)) by MSATERM:def 5;
then t in the Sorts of (FreeMSA X) . (the_sort_of u) by MSAFREE:def 11;
then t in the Sorts of (Free (S,X)) . (the_sort_of u) by MSAFREE3:31;
hence the_sort_of t = the_sort_of u by SORT; :: thesis: verum