let C, D be Category; :: thesis: for T being Functor of C,D
for c, c' being Object of C
for f being set st f in Hom c,c' holds
T . f in Hom (T . c),(T . c')
let T be Functor of C,D; :: thesis: for c, c' being Object of C
for f being set st f in Hom c,c' holds
T . f in Hom (T . c),(T . c')
let c, c' be Object of C; :: thesis: for f being set st f in Hom c,c' holds
T . f in Hom (T . c),(T . c')
let f be set ; :: thesis: ( f in Hom c,c' implies T . f in Hom (T . c),(T . c') )
assume A1: f in Hom c,c' ; :: thesis: T . f in Hom (T . c),(T . c')
then reconsider f' = f as Morphism of c,c' by Def7;
( dom f' = c & cod f' = c' ) by A1, Th18;
then ( T . c = dom (T . f') & T . c' = cod (T . f') ) by Th105;
hence T . f in Hom (T . c),(T . c') ; :: thesis: verum