[STATEMENT]
lemma comp: "bounded_clinear f \<Longrightarrow> bounded_clinear g \<Longrightarrow> bounded_cbilinear (\<lambda>x y. f x ** g y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bounded_clinear f; bounded_clinear g\<rbrakk> \<Longrightarrow> bounded_cbilinear (\<lambda>x y. f x ** g y)
[PROOF STEP]
by (rule bounded_cbilinear.flip[OF bounded_cbilinear.comp1[OF bounded_cbilinear.flip[OF comp1]]])