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:2;
then A1: ( Hom ((dom f),a) = {} implies Hom ((cod f),a) = {} ) by CAT_1:24;
( 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