let C be Category; :: thesis: for a being Object of C
for f being Morphism of C holds
( f in Hom a iff cod f = a )
let a be Object of C; :: thesis: for f being Morphism of C holds
( f in Hom a iff cod f = a )
let f be Morphism of C; :: thesis: ( f in Hom a iff cod f = a )
( Hom a = the Target of C " {a} & cod f = the Target of C . f & ( cod f in {a} implies cod f = a ) & ( cod f = a implies cod f in {a} ) ) by TARSKI:def 1;
hence ( f in Hom a iff cod f = a ) by FUNCT_2:46; :: thesis: verum