for p being Prime holds
( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) )