proposition: Lemma FunSET2_l_map_law : Map_law FunSET2_l_mor.
proof: Proof. unfold Map_law, FunSET2_l_mor in |- *. intros f1xg1 f2xg2; elim f1xg1; intros f1 g1. elim f2xg2; intros f2 g2; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold Equal_Pmor in |- *; simpl in |- *. unfold FunSET2_l_mor1 in |- *; simpl in |- *. unfold FunSET2_l_ob in |- *. intro H; elim H; intros H1 H2 h. apply Comp_lr. apply Comp_r; trivial. apply FPres. assumption. Qed.
imports: SET Dual PROD Functor