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 Th51;
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