let C, D be Category; :: thesis: for T being Functor of C,D
for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
let T be Functor of C,D; :: thesis: for c, c9 being Object of C
for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
let c, c9 be Object of C; :: thesis: for f being set st f in Hom (c,c9) holds
T . f in Hom ((T . c),(T . c9))
let f be set ; :: thesis: ( f in Hom (c,c9) implies T . f in Hom ((T . c),(T . c9)) )
assume A1: f in Hom (c,c9) ; :: thesis: T . f in Hom ((T . c),(T . c9))
then reconsider f9 = f as Morphism of c,c9 by Def3;
cod f9 = c9 by A1, Th1;
then A2: T . c9 = cod (T . f9) by Th64;
dom f9 = c by A1, Th1;
then T . c = dom (T . f9) by Th64;
hence T . f in Hom ((T . c),(T . c9)) by A2; :: thesis: verum