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

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