[STATEMENT]
lemma smc_FUNCT_components:
  shows "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Obj\<rparr> = cf_maps \<alpha> \<AA> \<BB>"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Arr\<rparr> = ntcf_arrows \<alpha> \<AA> \<BB>"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Dom\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>)"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Cod\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>)"
    and "smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Comp\<rparr> =
      (\<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>0\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Obj\<rparr> = cf_maps \<alpha> \<AA> \<BB> &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Arr\<rparr> = ntcf_arrows \<alpha> \<AA> \<BB>) &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Dom\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>) &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Cod\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>) &&& smc_FUNCT \<alpha> \<AA> \<BB>\<lparr>Comp\<rparr> = (\<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)
[PROOF STEP]
unfolding smc_FUNCT_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = cf_maps \<alpha> \<AA> \<BB> &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = ntcf_arrows \<alpha> \<AA> \<BB>) &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>) &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = (\<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>) &&& [cf_maps \<alpha> \<AA> \<BB>, ntcf_arrows \<alpha> \<AA> \<BB>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTDom\<rparr>, \<lambda>\<NN>\<in>\<^sub>\<circ>ntcf_arrows \<alpha> \<AA> \<BB>. \<NN>\<lparr>NTCod\<rparr>, \<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = (\<lambda>\<MM>\<NN>\<in>\<^sub>\<circ>composable_arrs (dg_FUNCT \<alpha> \<AA> \<BB>). \<MM>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F\<^bsub>\<AA>,\<BB>\<^esub> \<MM>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (simp_all add: nat_omega_simps)