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
Hom (T . c),(T . c9) <> {}
let T be Functor of C,D; :: thesis: for c, c9 being Object of C st Hom c,c9 <> {} holds
Hom (T . c),(T . c9) <> {}
let c, c9 be Object of C; :: thesis: ( Hom c,c9 <> {} implies Hom (T . c),(T . c9) <> {} )
consider f being Element of Hom c,c9;
assume Hom c,c9 <> {} ; :: thesis: Hom (T . c),(T . c9) <> {}
then f in Hom c,c9 ;
hence Hom (T . c),(T . c9) <> {} by Th123; :: thesis: verum