--- a/Quot/Examples/SigmaEx.thy	Tue Jan 26 15:59:04 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Tue Jan 26 16:30:51 2010 +0100
@@ -85,14 +85,14 @@
  \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
  \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
 
- Bexeq
-   (prod_rel (alpha_obj ===> op =)
+ Bex1
+   (Respects (prod_rel (alpha_obj ===> op =)
      (prod_rel (list_rel (prod_rel (op =) alpha_method) ===> op =)
        (prod_rel ((prod_rel (op =) alpha_method) ===> op =)
          (alpha_method ===> op =)
        )
      )
-   )
+   ))
 (\<lambda> (hom_o\<Colon>robj \<Rightarrow> 'a, hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b, hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c, hom_m\<Colon>rmethod \<Rightarrow> 'd).
 
 
@@ -128,6 +128,16 @@
 sorry
 
   
+lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))"
+apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects)
+apply clarify
+apply auto
+apply (rule bexI)
+apply assumption
+apply (simp add: in_respects)
+apply (simp add: in_respects)
+apply auto
+done
 
 lemma liftd: "
 Ex1 (\<lambda>(hom_o, hom_d, hom_e, hom_m).