f in Hom (a,b) by A1, CAT_1:def 5;
then T . f in Hom ((T . a),(T . b)) by CAT_1:81;
hence T . f is Morphism of T . a,T . b by CAT_1:def 5; :: thesis: verum