...

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 28b3795c88098743ba2648392ff77ef04c1244b1..dd6f9ae48f77ee8452b08fbb59226f9a7cd4634f 100644 (file)
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -56,7 +56,7 @@ ndefinition mmclosed ≝
    [ mk_magma_morphism _ p ⇒ p ].
  
 ndefinition sub_magma ≝
- λA.λM1,M2: magma A. ∀x. x ∈ mcarr ? M1 → x ∈ mcarr ? M2.
+ λA.λM1,M2: magma A. mcarr ? M1 ⊆ mcarr ? M2.
  
 ndefinition image: ∀A,B. (A → B) → Ω \sup A → Ω \sup B ≝
  λA,B,f,Sa. {y | ∃x. x ∈ Sa ∧ f x = y}.
@@ -68,9 +68,10 @@ ndefinition mm_image:
  #A; #B; #Ma; #Mb; #f;
  napply (mk_magma ???)
   [ napply (image ?? (mmcarr ?? (mmmcarr ???? f)) (mcarr ? Ma)) 
-  | #x; #y; *; #x0; #Hx0; *; #y0; #Hy0; nwhd;
+  | #x; #y; nwhd in ⊢ (% → % → ?); *; #x0; *; #Hx0; #Hx1; *; #y0; *; #Hy0; #Hy1; nwhd;
     napply (ex_intro ????)
      [ napply (op ? x0 y0) 
-     | napply (conj ????);
-       nelim daemon ]##]
+     | napply (conj ????)
+        [ napply (op_closed ??????); nassumption
+        | nelim daemon ]##]
 nqed.
\ No newline at end of file