[STATEMENT]
lemma comp_arr_point\<^sub>S\<^sub>C:
    assumes "arr f" and "\<guillemotleft>x : unity \<rightarrow> dom f\<guillemotright>"
    shows "f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
have "\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
arr f
\<guillemotleft>x : unity \<rightarrow> local.dom f\<guillemotright>

goal (1 subgoal):
 1. \<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>

goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>

goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
using assms Fun_def inj_img set_def
[PROOF STATE]
proof (prove)
using this:
\<guillemotleft>f \<cdot> x : unity \<rightarrow> cod f\<guillemotright>
arr f
\<guillemotleft>x : unity \<rightarrow> local.dom f\<guillemotright>
Fun ?f = restrict (img \<circ> (\<cdot>) ?f \<circ> inv_into (hom unity (local.dom ?f)) img) (local.set (local.dom ?f))
ide ?a \<Longrightarrow> inj_on img (hom unity ?a)
local.set ?a = img ` hom unity ?a

goal (1 subgoal):
 1. f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f \<cdot> x = inv_into (hom unity (cod f)) img (Fun f (img x))

goal:
No subgoals!
[PROOF STEP]
qed