( 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