--- a/Quot/QuotScript.thy	Thu Jan 07 16:51:38 2010 +0100
+++ b/Quot/QuotScript.thy	Fri Jan 08 10:08:01 2010 +0100
@@ -502,6 +502,13 @@
   using a b unfolding Respects_def
   by simp
 
+lemma abs_o_rep:
+  assumes a: "Quotient r absf repf"
+  shows "absf o repf = id"
+  apply(rule ext)
+  apply(simp add: Quotient_abs_rep[OF a])
+  done
+
 lemma fun_rel_eq_rel:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"