for p being Prime
for x, y being Element of (Z/Z* p)
for x1, y1 being Element of (INT.Ring p) st x = x1 & y = y1 holds
x * y = x1 * y1 by Lm12;