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 T . f is Morphism of T . c,T . c9
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 T . f is Morphism of T . c,T . c9
let c, c9 be Object of C; :: thesis: ( Hom c,c9 <> {} implies for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9 )
assume A1: Hom c,c9 <> {} ; :: thesis: for f being Morphism of c,c9 holds T . f is Morphism of T . c,T . c9
let f be Morphism of c,c9; :: thesis: T . f is Morphism of T . c,T . c9
T . f in Hom (T . c),(T . c9) by A1, Th124;
hence T . f is Morphism of T . c,T . c9 by Def7; :: thesis: verum