[STATEMENT]
lemma smcf_proj_components:
  shows "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>). a\<lparr>i\<rparr>)"
    and "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>(\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>). f\<lparr>i\<rparr>)"
    and "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>HomDom\<rparr> = (\<Prod>\<^sub>S\<^sub>M\<^sub>Ci\<in>\<^sub>\<circ>I. \<AA> i)"
    and "(\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i)\<lparr>HomCod\<rparr> = \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) &&& \<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>)) &&& \<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>HomDom\<rparr> = smc_prod I \<AA> &&& \<pi>\<^sub>S\<^sub>M\<^sub>C I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
[PROOF STEP]
unfolding smcf_proj_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>)) &&& [\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = smc_prod I \<AA> &&& [\<lambda>a\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, smc_prod I \<AA>, \<AA> i]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<AA> i
[PROOF STEP]
by (simp_all add: nat_omega_simps)