rw [bilinearComp_apply, bilinearComp_apply]
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂)) f) x +
      ((bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂)) f) x =
    f.1 x.1 + f.2 x.2
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((flip (apply R F)) ((fst R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((fst R M₁ M₂) x) +
      ((flip (apply R F)) ((snd R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((snd R M₁ M₂) x) =
    f.1 x.1 + f.2 x.2