proposition: Lemma S_together_map_law : Map_law S_together_fun.
proof: Proof. unfold Map_law in |- *. intros c1 c2 H; unfold S_together_fun in |- *; simpl in |- *. unfold Equal_Sprod in |- *; simpl in |- *; split; apply Pres1; trivial. Qed.
imports: SetoidPROD Binary_Products SET