∀[m,n:ℕ].  ((m ⋅ n) = (m * n) ∈ ℕ)
{ ((RepD) THENA Auto) }
1. m : ℕ
2. n : ℕ
⊢ (m ⋅ n) = (m * n) ∈ ℕ