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