[STATEMENT]
lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
  for f :: "_ \<Rightarrow> 'a::real_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))
[PROOF STEP]
unfolding continuous_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<longlongrightarrow> f (Lim F (\<lambda>x. x))) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p (f (Lim F (\<lambda>x. x)))) F
[PROOF STEP]
by (rule tendsto_poly)