ext
case h.e'_1
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ (fun n => s n * t n) = fun n => s n * (t n + -b) + b * s n
case h.e'_1.h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
x✝ : ℕ
⊢ s x✝ * t x✝ = s x✝ * (t x✝ + -b) + b * s x✝