∀ {α : Type u_1} (E : Type u_2) [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NormedAddCommGroup E] (x y : ↥(lp (fun x => E) ⊤)),
  AddEquiv.lpBCF.toFun (x + y) = AddEquiv.lpBCF.toFun x + AddEquiv.lpBCF.toFun y