{F : Type u_1} →
  {R : Type u_2} →
    {E₁ : Type u_3} →
      {E₂ : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid E₁] →
            [inst_2 : PartialOrder E₁] →
              [inst_3 : AddCommMonoid E₂] →
                [inst_4 : PartialOrder E₂] →
                  [inst_5 : Module R E₁] →
                    [inst_6 : Module R E₂] →
                      [inst_7 : FunLike F E₁ E₂] →
                        [LinearMapClass F R E₁ E₂] → [OrderHomClass F E₁ E₂] → F → E₁ →ₚ[R] E₂