let C be Category; :: thesis: for a being Object of C
for f being Morphism of C holds
( f in a Hom iff dom f = a )
let a be Object of C; :: thesis: for f being Morphism of C holds
( f in a Hom iff dom f = a )
let f be Morphism of C; :: thesis: ( f in a Hom iff dom f = a )
( dom f in {a} iff dom f = a ) by TARSKI:def 1;
hence ( f in a Hom iff dom f = a ) by FUNCT_2:38; :: thesis: verum