src/HOL/Analysis/Linear_Algebra.thy

     and f :: "'d::t2_space \<Rightarrow> 'a"
   assumes "continuous_on S f" "continuous_on S g" "bilinear h"
   shows "continuous_on S (\<lambda>x. h (f x) (g x))"
   using assms by (simp add: continuous_on_eq_continuous_within bilinear_continuous_compose)
 
-
 end