theorem Ex1: :: MOEBIUS2:27

for p being Prime holds 1 in FreeGen p