[STATEMENT]
lemma coprod_qbs_canonical1':
  assumes "countable I"
      and "\<And>i. i \<in> I \<Longrightarrow> (\<lambda>x. f (i,x)) \<in> X i \<rightarrow>\<^sub>Q Y"
    shows  "f \<in> (\<amalg>\<^sub>Q i \<in>I. X i) \<rightarrow>\<^sub>Q Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> coprod_qbs I X \<rightarrow>\<^sub>Q Y
[PROOF STEP]
using coprod_qbs_canonical1[where f="curry f"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>countable ?I; \<And>i. i \<in> ?I \<Longrightarrow> curry f i \<in> ?X i \<rightarrow>\<^sub>Q ?Y\<rbrakk> \<Longrightarrow> (\<lambda>(i, x). curry f i x) \<in> coprod_qbs ?I ?X \<rightarrow>\<^sub>Q ?Y
countable I
?i \<in> I \<Longrightarrow> (\<lambda>x. f (?i, x)) \<in> X ?i \<rightarrow>\<^sub>Q Y

goal (1 subgoal):
 1. f \<in> coprod_qbs I X \<rightarrow>\<^sub>Q Y
[PROOF STEP]
by(auto simp: curry_def)