proposition: Lemma nthom_bounded : forall f g, Bounded.axioms (nthom f g).
proof: Proof. ir. cp (Bounded.trans_criterion (p:=nthom f g) (f:= fun u => Arrow.create f g (ntrans_arrow_create f (fun y => V y u))) (x:= Function_Set.function_set (objects (source f)) (fun z => morphisms (target g)))). ap H. ir. sh (L (objects (source f)) (ntrans y)). ee. apply Function_Set.in_function_set_inc. apply Function_Set.in_fs_for_L. ir. assert (ob (source f) y0). ap is_ob_ob. uh H0; ee. wr H2. uh H0; ee. exact H4. am. change (is_mor (target g) (ntrans y y0)). ap mor_is_mor. ap mor_ntrans. lu. uh H0; ee. uf osource. rw H3. am. uf otarget. uh H0; ee. rw H4. tv. uh H0; ee. assert (Nat_Trans.like y). lu. uh H3; ee. ufi create H3. set (k:=ntrans y). wr H3. uf k. wr H1. wr H2. ap uneq. uf ntrans_arrow_create. assert (Function.create (objects (source (source y))) (fun y0 : E => V y0 (Function.create (objects (source (source y))) (ntrans y))) = Function.create (objects (source (source y))) (ntrans y)). ap Function.create_extensionality. tv. ir. rw create_V_rewrite. tv. am. rww H4. Qed.
imports: Arith nat_trans