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 A1: ( Hom (dom f),a = {} implies Hom (cod f),a = {} ) by CAT_1:52;
( Hom (dom f),a in Hom C & Hom (cod f),a in Hom C ) ;
hence [[(Hom (cod f),a),(Hom (dom f),a)],(hom f,a)] is Element of Maps (Hom C) by A1, Th5; :: thesis: verum