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