proposition: Lemma S_lambda_map_law1 : Map_law S_lambda_fun1.
proof: Proof. unfold Map_law in |- *. intros c1 c2 H; unfold S_lambda_fun1 in |- *; simpl in |- *. unfold Ext in |- *; intro a; unfold S_lambda_fun2 in |- *; simpl in |- *. apply Pres1. simpl in |- *; unfold Equal_Sprod in |- *; simpl in |- *; split. trivial. apply Refl. Qed.
imports: SET_BinProds Exponents