[STATEMENT]
lemma setsetmapim_comp: "(f\<circ>g)\<turnstile>A = f\<turnstile>(g\<turnstile>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<circ> g) \<turnstile> A = f \<turnstile> (g \<turnstile> A)
[PROOF STEP]
by (auto simp add: image_comp)