∀ {𝕜 : Type u_2} {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E]
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [inst_5 : IsScalarTower ℝ 𝕜 E] [inst_6 : ContinuousConstSMul 𝕜 E],
  (∀ (fr : StrongDual ℝ E) (x : E),
      ((fun fr =>
              let __LinearMap := (↑fr).extendTo𝕜';
              { toLinearMap := __LinearMap, cont := ⋯ })
            fr)
          x =
        ↑(fr x) - RCLike.I * ↑(fr (RCLike.I • x))) →
    ∀ (x y : StrongDual ℝ E),
      (fun fr =>
            let __LinearMap := (↑fr).extendTo𝕜';
            { toLinearMap := __LinearMap, cont := ⋯ })
          (x + y) =
        (fun fr =>
              let __LinearMap := (↑fr).extendTo𝕜';
              { toLinearMap := __LinearMap, cont := ⋯ })
            x +
          (fun fr =>
              let __LinearMap := (↑fr).extendTo𝕜';
              { toLinearMap := __LinearMap, cont := ⋯ })
            y