theorem Th21: :: INT_7:21
for p being Prime holds
( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) )