From be8d8e78f342e13043ef659d5f9f944d343325f4 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Jul 2009 07:42:01 +0000
Subject: [PATCH] ...

---
 helm/software/matita/nlibrary/algebra/magmas.ma | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 28b3795c8..dd6f9ae48 100644
--- 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
-- 
2.39.2