let C be Category; :: thesis: for a being Object of C
for f being Morphism of C holds [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C)
let a be Object of C; :: thesis: for f being Morphism of C holds [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C)
let f be Morphism of C; :: thesis: [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C)
Hom (dom f),(cod f) <> {} by CAT_1:19;
then ( ( Hom (dom f),a = {} implies Hom (cod f),a = {} ) & Hom (dom f),a in Hom C & Hom (cod f),a in Hom C ) by CAT_1:52;
hence [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C) by Th5; :: thesis: verum