( T is Function of the carrier' of C,the carrier' of D & Hom c,c' c= the carrier' of C & 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