apply ContinuousOn.comp (g := deriv ζ) ?_ ?_ (mapsTo_image _ _)
case hcont
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => deriv ζ (↑y + ↑t * I)) [[σ₁, σ₂]]
σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (deriv ζ) ((fun y => ↑y + ↑t * I) '' [[σ₁, σ₂]])

σ₁ σ₂ t : ℝ
t_ne_zero : t ≠ 0
diff : ∀ (σ : ℝ), DifferentiableAt ℂ ζ (↑σ + ↑t * I)
⊢ ContinuousOn (fun y => ↑y + ↑t * I) [[σ₁, σ₂]]