unfold RectangleIntegral VIntegral
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ RectangleIntegral f z w = RectangleIntegral g z w
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
h : EqOn f g (RectangleBorder z w)
⊢ (HIntegral f z.re w.re z.im - HIntegral f z.re w.re w.im + I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * I) =
    (HIntegral g z.re w.re z.im - HIntegral g z.re w.re w.im + I • ∫ (y : ℝ) in z.im..w.im, g (↑w.re + ↑y * I)) -
      I • ∫ (y : ℝ) in z.im..w.im, g (↑z.re + ↑y * I)