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

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