theorem Lm1: :: MOEBIUS2:34

for p being Prime
for n being non zero Nat st n in FreeGen p holds
support (pfexp n) c= Seg p