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