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