[STATEMENT]
lemma IdFtor'Obj:
  assumes "Category C" and "X \<in> obj\<^bsub>CatDom (FId' C)\<^esub>"
  shows "(FId' C) @@ X = X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
have "(FId' C) ## id\<^bsub>CatDom (FId' C)\<^esub> X = id\<^bsub>CatCod (FId' C)\<^esub> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
[PROOF STEP]
by(simp add: IdentityFunctor'_def)
[PROOF STATE]
proof (state)
this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
have "X \<in> obj\<^bsub>CatCod (FId' C)\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<in> obj\<^bsub>CatCod FId' C\<^esub>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Category C
X \<in> obj\<^bsub>CatDom FId' C\<^esub>

goal (1 subgoal):
 1. X \<in> obj\<^bsub>CatCod FId' C\<^esub>
[PROOF STEP]
by (simp add: IdentityFunctor'_def)
[PROOF STATE]
proof (state)
this:
X \<in> obj\<^bsub>CatCod FId' C\<^esub>

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
X \<in> obj\<^bsub>CatCod FId' C\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
X \<in> obj\<^bsub>CatCod FId' C\<^esub>

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
FId' C ## id\<^bsub>CatDom FId' C\<^esub> X = id\<^bsub>CatCod FId' C\<^esub> X
X \<in> obj\<^bsub>CatCod FId' C\<^esub>
Category C
X \<in> obj\<^bsub>CatDom FId' C\<^esub>

goal (1 subgoal):
 1. FId' C @@ X = X
[PROOF STEP]
by (simp add: PreFunctor.FmToFo IdFtor'PreFunctor)
[PROOF STATE]
proof (state)
this:
FId' C @@ X = X

goal:
No subgoals!
[PROOF STEP]
qed