let p be Prime; :: thesis: card (Z/ p) = p
set F = Z/ p;
set M = MultGroup (Z/ p);
MultGroup (Z/ p) = Z/Z* p by GR_CY_3:36;
then A: card (MultGroup (Z/ p)) = p - 1 by INT_7:23;
card (MultGroup (Z/ p)) = (card (Z/ p)) - 1 by UNIROOTS:18;
hence card (Z/ p) = p by A; :: thesis: verum