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)) <> {} )
set f = the Element of Hom (c,c9);
assume Hom (c,c9) <> {} ; :: thesis: Hom ((T . c),(T . c9)) <> {}
then the Element of Hom (c,c9) in Hom (c,c9) ;
hence Hom ((T . c),(T . c9)) <> {} by Th76; :: thesis: verum