[STATEMENT]
lemma uniformly_convergent_minus:
  "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
      uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>uniformly_convergent_on A f; uniformly_convergent_on A g\<rbrakk> \<Longrightarrow> uniformly_convergent_on A (\<lambda>k x. f k x - g k x)
[PROOF STEP]
unfolding uniformly_convergent_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>l. uniform_limit A f l sequentially; \<exists>l. uniform_limit A g l sequentially\<rbrakk> \<Longrightarrow> \<exists>l. uniform_limit A (\<lambda>k x. f k x - g k x) l sequentially
[PROOF STEP]
by (blast dest: uniform_limit_minus)