Theorem nmul_neutr

Proof
nmul_neutr. ⊢ a ∈ ℕ → a⋅1 = a,
  pred_restr nat_incl_in_real rmul_neutr.

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