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