x -term in T by Th24;
then reconsider xt = x -term as Element of T ;
the_sort_of xt = the_sort_of (@ xt) by Lem00;
hence (canonical_homomorphism T) . (x -term) = x -term ; :: thesis: verum