let A be Category; :: thesis: for a being Object of A
for m being Morphism of a,a holds m in Hom a,a
let a be Object of A; :: thesis: for m being Morphism of a,a holds m in Hom a,a
let m be Morphism of a,a; :: thesis: m in Hom a,a
Hom a,a <> {} by CAT_1:56;
hence m in Hom a,a by CAT_1:def 7; :: thesis: verum