for p being Prime
for x being Element of (Z/Z* p)
for x1 being Element of (INT.Ring p) st x = x1 holds
x " = x1 "