Lemma M1_is_CSemiGroup:(is_CSemiGroup M1_as_CSetoid M1_mult_as_bin_fun).
Lemma e1_is_lft_unit: (is_lft_unit M1_mult_as_bin_fun e1).
Lemma e1_is_rht_unit:(is_rht_unit M1_mult_as_bin_fun e1).
Definition M1_as_CSemiGroup:CSemiGroup:=
(Build_CSemiGroup M1_as_CSetoid M1_mult_as_bin_fun M1_is_CSemiGroup).
Lemma M2_is_CSemiGroup:(is_CSemiGroup M1_as_CSetoid M2_mult_as_bin_fun).
Definition M2_as_CSemiGroup:=
(Build_CSemiGroup M1_as_CSetoid M2_mult_as_bin_fun M2_is_CSemiGroup).
Lemma e1_is_lft_unit_M2: (is_lft_unit M2_mult_as_bin_fun e1).
Lemma e1_is_rht_unit_M2: (is_rht_unit M2_mult_as_bin_fun e1).
End p68E1b1.