theorem Th22: :: NUMBER16:22

for n being non zero Nat holds
( ( rng (pfexp n) c= {0,1} & card (support (pfexp n)) = 1 ) iff n is prime )