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