let p be Prime; :: thesis: card (Z/Z* p) = p - 1
1 < p by INT_2:def 4;
hence card (Z/Z* p) = p - 1 by Th18; :: thesis: verum