H₂( <NAT,+,0> ) = H₂( <NAT,+> ) by Th18;
then <NAT,+,0> is SubStr of <NAT,+> by Def23;
hence for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,+,0> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 + n2 by Th39; :: thesis: verum