theorem LmRng: :: MOEBIUS2:36

for n being non zero square-free Nat holds rng (pfexp n) c= 2