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 )
( a Hom = the Source of C " {a} & dom f = the Source of C . f & ( dom f in {a} implies dom f = a ) & ( dom f = a implies dom f in {a} ) ) by TARSKI:def 1;
hence ( f in a Hom iff dom f = a ) by FUNCT_2:46; :: thesis: verum