Proof of Law Packages for the Operations of ℕ₀ and of a Commutative Ring

For (i): $+$ is a binary operation on $\mathbb{N}_{0}$ whose value at $(m,n)$ is the sum $m+n\in\mathbb{N}_{0}$, by Addition on Omega (i), and $\cdot$ is one whose value at $(m,n)$ is the product $m\cdot n\in\mathbb{N}_{0}$, by Multiplication on Omega: Products Lie in Omega, Multiplication Is a Binary Operation with Value the Product, and Membership in the Multiplication (ii) and Multiplication on Omega: Products Lie in Omega, Multiplication Is a Binary Operation with Value the Product, and Membership in the Multiplication (i); also $0,1\in\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii). So the laws are identities between sums and products in $\mathbb{N}_{0}$. For $+$, associativity, commutativity and $0+m=m=m+0$ are Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iii), Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (iv) and Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order (i). For $\cdot$, they are Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (v), Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (vi) and Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order (iii), the last because $1$ is the successor of $0$ by The Set of Natural Numbers and the Number One (ii).

For (ii): by Commutative Rings (i), $+$ and $\cdot$ are binary operations on $R$ and $0,1\in R$, and its identities give, for all $x,y,z\in R$, associativity and commutativity of both operations, $x+0=x$ and $x\cdot1=x$; commutativity then gives $0+x=x$ and $1\cdot x=x$.