[STATEMENT]
lemma YFtorObj: 
  assumes "LSCategory C" and "X \<in> Obj C"
  shows "(YFtor C) @@ X = Hom\<^bsub>C \<^esub>[\<midarrow>,X]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
have "CatDom (YFtor' C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CatDom (YFtor' C) = C
[PROOF STEP]
by (simp add: YFtor'_def)
[PROOF STATE]
proof (state)
this:
CatDom (YFtor' C) = C

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CatDom (YFtor' C) = C

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
hence "(YFtor' C) @@ X = Hom\<^bsub>C \<^esub>[\<midarrow>,X]"
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C

goal (1 subgoal):
 1. YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C
LSCategory C
X \<in> obj\<^bsub>C\<^esub>

goal (1 subgoal):
 1. YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
by(simp add: YFtor'Obj)
[PROOF STATE]
proof (state)
this:
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
have "PreFunctor (YFtor' C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PreFunctor (YFtor' C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LSCategory C
X \<in> obj\<^bsub>C\<^esub>

goal (1 subgoal):
 1. PreFunctor (YFtor' C)
[PROOF STEP]
by (simp add: YFtorPreFtor)
[PROOF STATE]
proof (state)
this:
PreFunctor (YFtor' C)

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CatDom (YFtor' C) = C
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
PreFunctor (YFtor' C)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
PreFunctor (YFtor' C)

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CatDom (YFtor' C) = C
YFtor' C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
PreFunctor (YFtor' C)
LSCategory C
X \<in> obj\<^bsub>C\<^esub>

goal (1 subgoal):
 1. YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]
[PROOF STEP]
by (simp add: MakeFtorObj YFtor_def)
[PROOF STATE]
proof (state)
this:
YFtor C @@ X = Hom\<^bsub>C\<^esub>[\<midarrow>,X]

goal:
No subgoals!
[PROOF STEP]
qed