let C, D be Category; :: thesis: for T being Functor of C,D
for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
let T be Functor of C,D; :: thesis: for c, c9 being Object of C st Hom (c,c9) <> {} holds
for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
let c, c9 be Object of C; :: thesis: ( Hom (c,c9) <> {} implies for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f )
assume A1: Hom (c,c9) <> {} ; :: thesis: for f being Morphism of c,c9 holds (hom (T,c,c9)) . f = T . f
let f be Morphism of c,c9; :: thesis: (hom (T,c,c9)) . f = T . f
f in Hom (c,c9) by A1, Def3;
hence (hom (T,c,c9)) . f = T . f by FUNCT_1:49; :: thesis: verum