let C, D be Category; :: thesis: for T being Functor of C,D
for c, c' being Object of C st Hom c,c' <> {} holds
for f being Morphism of c,c' holds (hom T,c,c') . f = T . f
let T be Functor of C,D; :: thesis: for c, c' being Object of C st Hom c,c' <> {} holds
for f being Morphism of c,c' holds (hom T,c,c') . f = T . f
let c, c' be Object of C; :: thesis: ( Hom c,c' <> {} implies for f being Morphism of c,c' holds (hom T,c,c') . f = T . f )
assume A1: Hom c,c' <> {} ; :: thesis: for f being Morphism of c,c' holds (hom T,c,c') . f = T . f
let f be Morphism of c,c'; :: thesis: (hom T,c,c') . f = T . f
( T is Function of the carrier' of C,the carrier' of D & f in Hom c,c' ) by A1, Def7;
hence (hom T,c,c') . f = T . f by FUNCT_1:72; :: thesis: verum