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:27;
hence m in Hom (a,a) by CAT_1:def 4; :: thesis: verum