[STATEMENT]
lemma cmp_fun_image:"\<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C \<rbrakk> \<Longrightarrow>
                          (cmp g f) ` A =  g ` (f ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> cmp g f ` A = g ` f ` A
[PROOF STEP]
apply (rule equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> cmp g f ` A \<subseteq> g ` f ` A
 2. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> g ` f ` A \<subseteq> cmp g f ` A
[PROOF STEP]
apply (rule subsetI, simp add:image_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; \<exists>xa\<in>A. x = cmp g f xa\<rbrakk> \<Longrightarrow> \<exists>xa. (\<exists>x\<in>A. xa = f x) \<and> x = g xa
 2. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> g ` f ` A \<subseteq> cmp g f ` A
[PROOF STEP]
apply (erule bexE, simp add:cmp_def, blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C\<rbrakk> \<Longrightarrow> g ` f ` A \<subseteq> cmp g f ` A
[PROOF STEP]
apply (rule subsetI, simp add:image_def[of g])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; \<exists>xa\<in>A. x = g (f xa)\<rbrakk> \<Longrightarrow> x \<in> cmp g f ` A
[PROOF STEP]
apply (erule bexE, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; xa \<in> A; x = g (f xa)\<rbrakk> \<Longrightarrow> g (f xa) \<in> cmp g f ` A
[PROOF STEP]
apply (simp add:image_def cmp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>f \<in> A \<rightarrow> B; g \<in> B \<rightarrow> C; xa \<in> A; x = g (f xa)\<rbrakk> \<Longrightarrow> \<exists>x\<in>A. g (f xa) = g (f x)
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done