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