let C be Category; :: thesis: for a being Object of
for f being Morphism of holds
( f in Hom a iff cod f = a )
let a be Object of ; :: thesis: for f being Morphism of holds
( f in Hom a iff cod f = a )
let f be Morphism of ; :: 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:46; :: thesis: verum