let C be Category; :: thesis: for f, g being Morphism of C holds [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C)
let f, g be Morphism of C; :: thesis: [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C)
A1: ( Hom ((dom f),(cod g)) in Hom C & Hom ((cod f),(dom g)) in Hom C ) ;
( Hom ((dom f),(cod g)) = {} implies Hom ((cod f),(dom g)) = {} ) by Th50;
hence [[(Hom ((cod f),(dom g))),(Hom ((dom f),(cod g)))],(hom (f,g))] is Element of Maps (Hom C) by A1, Th5; :: thesis: verum