proposition: Lemma S_lambda_map_law : Map_law S_lambda1_fun.
proof: Proof. unfold Map_law in |- *. intros f g H; unfold S_lambda1_fun in |- *; simpl in |- *. unfold Ext in |- *; simpl in |- *; intros c. unfold Ext in |- *; simpl in |- *; intro a. unfold S_lambda_fun2 in |- *. apply (H (Build_Sprod c a)). Qed.
imports: SET_BinProds Exponents