theorem corollary_22_6 {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] (Δ : TriangularDecomposition R 𝔤) (wg : WeylGroupData Δ) (lam : ↥Δ.𝔥 →ₗ[R] R) : (∀ (F₁ F₂ : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F₁ → ProjectiveFunctors.IsProjectiveFunctor F₂ → ∀ (Mverma : ProjectiveFunctors.RepGfObj R 𝔤), Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) → ∀ (iso_fwd : ProjectiveFunctors.RepGfHom (F₁.obj Mverma) (F₂.obj Mverma)) (iso_bwd : ProjectiveFunctors.RepGfHom (F₂.obj Mverma) (F₁.obj Mverma)), (iso_bwd.comp iso_fwd).EqAsMap (ProjectiveFunctors.RepGfHom.id (F₁.obj Mverma)) → (iso_fwd.comp iso_bwd).EqAsMap (ProjectiveFunctors.RepGfHom.id (F₂.obj Mverma)) → ProjectiveFunctors.AreNatIsoOnGenInfChar lam F₁ F₂) ∧ (∀ (F : ProjectiveFunctors.EndoFunctorData R 𝔤), ProjectiveFunctors.IsProjectiveFunctor F → ∀ (Mverma : ProjectiveFunctors.RepGfObj R 𝔤), Nonempty (IsVermaModule Δ Mverma.carrier (lam - wg.ρ)) → ∀ (n : ℕ) (summands : Fin n → ProjectiveFunctors.RepGfObj R 𝔤), ProjectiveFunctors.IsDirectSumDecompObj (F.obj Mverma) summands → ∃ (F_i : Fin n → ProjectiveFunctors.EndoFunctorData R 𝔤), (∀ (i : Fin n), ProjectiveFunctors.IsProjectiveFunctor (F_i i)) ∧ (∀ (i : Fin n), (F_i i).obj Mverma = summands i) ∧ ProjectiveFunctors.IsDirectSumDecomp F F_i) ∧ ∀ (H : ProjectiveFunctors.ThetaFunctorData R 𝔤 Δ wg lam), ProjectiveFunctors.IsProjectiveThetaFunctor H → ∃ (F : ProjectiveFunctors.EndoFunctorData R 𝔤) (_ : ProjectiveFunctors.IsProjectiveFunctor F) (T : ProjectiveFunctors.ThetaFunctorData R 𝔤 Δ wg lam), T.baseFunctor = F ∧ ProjectiveFunctors.AreNatIsoTheta H T