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