theorem :: MOEBIUS2:28

for p being Prime holds not 0 in FreeGen p by MOEBIUS1:21, FG;