( Hom ((dom f),(cod f)) <> {} & f is Morphism of dom f, cod f ) by CAT_1:19, CAT_1:22;
hence (curry (F,f)) * the Id of B is natural_transformation of F ?- (dom f),F ?- (cod f) by Th17; :: thesis: verum