∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] (n : ℕ) (f : C(↑unitInterval, E)) (x : ↑unitInterval),
  (bernsteinApproximation n f) x = ∑ k, (bernstein n ↑k) x • f (bernstein.z k)