∀ (R : Type u_1) [inst : CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {a b : ℕ → R},
  a ∈ (Perfection.submonoid R p).carrier →
    b ∈ (Perfection.submonoid R p).carrier → ∀ (n : ℕ), (frobenius R p) (a (n + 1) + b (n + 1)) = (a + b) n