the_sort_of (@ r) = the_sort_of r by Lem00;
then r in the Sorts of T . (the_sort_of (@ r)) by SORT;
then ((canonical_homomorphism T) . (the_sort_of (@ r))) . (@ r) = r by MSAFREE4:47;
hence (canonical_homomorphism T) . (@ r) = r by ABBR; :: thesis: verum