T .: (Hom c,c') c= Hom (T . c),(T . c') by Th129;
hence T | (Hom c,c') is Function of (Hom c,c'),(Hom (T . c),(T . c')) by FUNCT_2:178; :: thesis: verum