[STATEMENT]
lemma zcf_mult:
  assumes "p \<in> carrier P"
  assumes "q \<in> carrier P"
  shows "zcf(p \<otimes>\<^bsub>P\<^esub> q) = (zcf p) \<otimes> (zcf q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zcf (p \<otimes>\<^bsub>P\<^esub> q) = zcf p \<otimes> zcf q
[PROOF STEP]
using zcf_to_fun[of " p \<otimes>\<^bsub>P\<^esub> q" ] zcf_to_fun[of "p" ] zcf_to_fun[of "q" ] to_fun_mult[of q p \<zero>]
[PROOF STATE]
proof (prove)
using this:
p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P \<Longrightarrow> zcf (p \<otimes>\<^bsub>P\<^esub> q) = to_fun (p \<otimes>\<^bsub>P\<^esub> q) \<zero>
p \<in> carrier P \<Longrightarrow> zcf p = to_fun p \<zero>
q \<in> carrier P \<Longrightarrow> zcf q = to_fun q \<zero>
\<lbrakk>q \<in> carrier P; p \<in> carrier P; \<zero> \<in> carrier R\<rbrakk> \<Longrightarrow> to_fun (p \<otimes>\<^bsub>P\<^esub> q) \<zero> = to_fun p \<zero> \<otimes> to_fun q \<zero>

goal (1 subgoal):
 1. zcf (p \<otimes>\<^bsub>P\<^esub> q) = zcf p \<otimes> zcf q
[PROOF STEP]
by (simp add: assms(1) assms(2))