proposition: Lemma Fun_comp_law : Fcomp_law FunSET_map.
proof: Proof. unfold Fcomp_law in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *. unfold Comp_fun in |- *; simpl in |- *. unfold FunSET_mor1, FunSET_ob in |- *. intros b c d f g h. apply Ass. Qed.
imports: SET Functor Dual