∀ {M : Type u_5} {ι : Type u_6} {α : ι → Type u_7} [inst : AddMonoid M] [inst_1 : (i : ι) → AddAction M (α i)] {c : M},
  IsAddUnit c → ∀ (I : Set ι) (s : (i : ι) → Set (α i)), c +ᵥ I.pi s = I.pi (c +ᵥ s)