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