Theorem nmul_distl_add

Proof
nmul_distl_add. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a⋅(b + c) = a⋅b + a⋅c,
  pred_iii_restr nat_incl_in_real rmul_distl_add.

Dependencies
The given proof depends on five axioms:
comp, eq_subst, radd_closed, real_is_set, rmul_distl_add.