∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (hpq : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F}, LinearMap.ofIsCompl hpq φ ψ = φ ∘ₗ p.linearProjOfIsCompl q hpq + ψ ∘ₗ q.linearProjOfIsCompl p ⋯