let C be Category; 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; 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; [[(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; verum