let C, D be Category; 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; 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; T .: (Hom (c,c9)) c= Hom ((T . c),(T . c9))
let f be object ; TARSKI:def 3 ( not f in T .: (Hom (c,c9)) or f in Hom ((T . c),(T . c9)) )
assume
f in T .: (Hom (c,c9))
; 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; verum