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 object ; :: 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:65;
hence f in Hom ((T . c),(T . c9)) by Th76; :: thesis: verum