# HG changeset patch
# User lcp
# Date 757936791 -3600
# Node ID be834b9a0c7285c69a27f57ee3a99e767b7ae930
# Parent  c972c57e7762a2d183ad033ff73d8110fffdaae8
ZF/perm/image_comp: new

diff -r c972c57e7762 -r be834b9a0c72 src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Wed Jan 05 19:47:14 1994 +0100
+++ b/src/ZF/Perm.ML	Fri Jan 07 10:59:51 1994 +0100
@@ -194,6 +194,11 @@
 by (fast_tac comp_cs 1);
 val domain_comp_eq = result();
 
+goal Perm.thy "(r O s)``A = r``(s``A)";
+by (fast_tac (comp_cs addIs [equalityI]) 1);
+val image_comp = result();
+
+
 (** Other results **)
 
 goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
diff -r c972c57e7762 -r be834b9a0c72 src/ZF/perm.ML
--- a/src/ZF/perm.ML	Wed Jan 05 19:47:14 1994 +0100
+++ b/src/ZF/perm.ML	Fri Jan 07 10:59:51 1994 +0100
@@ -194,6 +194,11 @@
 by (fast_tac comp_cs 1);
 val domain_comp_eq = result();
 
+goal Perm.thy "(r O s)``A = r``(s``A)";
+by (fast_tac (comp_cs addIs [equalityI]) 1);
+val image_comp = result();
+
+
 (** Other results **)
 
 goal Perm.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";