theorem :: INT_7:23

for p being Prime holds card (Z/Z* p) = p - 1 by INT_2:def 4, Th18;