theorem :: MOEBIUS3:48

for n being non zero Nat holds support (pfexp n) c= Seg n