let C, D be Category; :: thesis: for T being Functor of C,D
for c, c9 being Object of C holds T .: (Hom c,c9) c= Hom (T . c),(T . c9)
let T be Functor of C,D; :: thesis: for c, c9 being Object of C holds T .: (Hom c,c9) c= Hom (T . c),(T . c9)
let c, c9 be Object of C; :: thesis: T .: (Hom c,c9) c= Hom (T . c),(T . c9)
let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in T .: (Hom c,c9) or f in Hom (T . c),(T . c9) )
assume f in T .: (Hom c,c9) ; :: thesis: f in Hom (T . c),(T . c9)
then ex g being Element of the carrier' of C st
( g in Hom c,c9 & f = T . g ) by FUNCT_2:116;
hence f in Hom (T . c),(T . c9) by Th123; :: thesis: verum