proposition: Lemma S_lambda_map_law2 : Map_law S_lambda_fun2.
proof: Proof. unfold Map_law in |- *. intros a1 a2 H; unfold S_lambda_fun2 in |- *. apply Pres1. simpl in |- *; unfold Equal_Sprod in |- *; simpl in |- *; split. apply Refl. trivial. Qed.
imports: SET_BinProds Exponents