+Instance MonoidalFullSubcategory_Monoidal `(mc:MonoidalCat) {Pobj} Pobj_unit Pobj_closed V
+ : MonoidalCat (PreMonoidalFullSubcategory_PreMonoidal(Pobj:=Pobj) mc V Pobj_unit Pobj_closed).
+ apply Build_MonoidalCat.
+ apply Build_CommutativeCat.
+ intros.
+ idtac.
+ apply Build_CentralMorphism; intros.
+ destruct a.
+ destruct b.
+ destruct c.
+ destruct d.
+ simpl.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=mon_commutative(MonoidalCat:=mc)) f)).
+
+ destruct a.
+ destruct b.
+ destruct c.
+ destruct d.
+ simpl.
+ apply (centralmor_first(CentralMorphism:=commutative_central(CommutativeCat:=mon_commutative(MonoidalCat:=mc)) g)).
+ Defined.
+