+ napply ex_intro
+ [ napply (op … x0 y0)
+ | napply conj
+ [ napply op_closed; nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop … f)]##]
+nqed.
+
+ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
+ λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
+
+ndefinition mm_counter_image:
+ ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism … Ma Mb → magma A.
+ #A; #B; #Ma; #Mb; #f;
+ napply mk_magma
+ [ napply (counter_image … f Mb)
+ | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
+ napply ex_intro
+ [ napply (op … x0 y0)
+ | napply conj
+ [ napply op_closed; nassumption
+ | nrewrite < Hx1;
+ nrewrite < Hy1;
+ napply (mmprop … f)]##]
+nqed.
+
+ndefinition m_intersect: ∀A. magma A → magma A → magma A.
+ #A; #M1; #M2;
+ napply (mk_magma …)
+ [ napply (M1 ∩ M2)
+ | #x; #y; nwhd in ⊢ (% → % → %); *; #Hx1; #Hx2; *; #Hy1; #Hy2;
+ napply conj; napply op_closed; nassumption ]