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 )
( cod f in {a} iff cod f = a ) by TARSKI:def 1;
hence ( f in Hom a iff cod f = a ) by FUNCT_2:38; :: thesis: verum