∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E),
  ∀ z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1,
    BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
      ‖f z‖ ≤ Complex.HadamardThreeLines.sSupNormIm f z.re