theorem fresh3a: :: FIELD_16:24

for p being Prime holds card (Z/ p) = p