∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : AddCommMonoid S]
  (p : SkewMonoidAlgebra k G) (f g : G → k → S), (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g