theorem :: MONOID_0:53

for n1, n2 being Element of NAT
for m1, m2 being Element of <NAT,*> st n1 = m1 & n2 = m2 holds
m1 * m2 = n1 * n2 by Th50;