( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:2, CAT_1:4;
hence (curry (F,f)) * (IdMap B) is natural_transformation of F ?- (dom f),F ?- (cod f) by Th13; :: thesis: verum