theorem :: MONOID_0:55

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