--- a/QuotScript.thy	Thu Oct 22 15:02:01 2009 +0200
+++ b/QuotScript.thy	Thu Oct 22 15:44:16 2009 +0200
@@ -474,10 +474,10 @@
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 lemma RES_FORALL_RSP:
-  assumes a: "QUOTIENT R absf repf"
   shows "\<And>f g. (R ===> (op =)) f g ==>
         (Ball (Respects R) f = Ball (Respects R) g)"
-  sorry
+  apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS)
+  done
 
 end