1082 (* alternative proof *)

  1083 lemma 

  1084   shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)"

  1085 proof (rule subsetCI)

  1086   fix a::"atom"

  1087   assume a: "a \<in> supp (f x)"

  1088   assume b: "a \<notin> supp f \<union> supp x"

  1089   then have "finite {b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f}" "finite {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x}" 

  1090     unfolding supp_def by auto

  1091   then have "finite ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})" by simp

  1092   moreover 

  1093   have "{b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x} \<subseteq> ({b. (a \<rightleftharpoons> b) \<bullet> f \<noteq> f} \<union> {b. (a \<rightleftharpoons> b) \<bullet> x \<noteq> x})"

  1094     by auto

  1095   ultimately have "finite {b. ((a \<rightleftharpoons> b) \<bullet> f) ((a \<rightleftharpoons> b) \<bullet> x) \<noteq> f x}"

  1096     using finite_subset by auto

  1097   then have "a \<notin> supp (f x)" unfolding supp_def

  1098     by (simp add: permute_fun_app_eq)

  1099   with a show "False" by simp

  1100 qed

  1101