proposition: Lemma S_eval_map_law : Map_law S_eval_fun.
proof: Proof. unfold Map_law in |- *. intros fxa gxa'; elim fxa; intros f a; elim gxa'; intros g a'; simpl in |- *. unfold S_eval_fun in |- *; simpl in |- *. unfold Equal_Sprod in |- *; simpl in |- *. intro H; elim H; intros H1 H2. apply Trans with (f a'). apply Pres1; trivial. apply (H1 a'). Qed.
imports: SET_BinProds Exponents