x -term in T by Th24;
then reconsider t = x -term as Element of T ;
( the_sort_of (x -term) = s & the_sort_of t = the_sort_of (@ t) ) by SORT, Lem00;
then t in the Sorts of T . s by SORT;
hence ((canonical_homomorphism T) . s) . (x -term) = x -term by MSAFREE4:47; :: thesis: verum