let p be Prime; :: thesis: (pfexp p) . p = 1
p = p |^ 1 by NEWTON:5;
hence (pfexp p) . p = 1 by Th40; :: thesis: verum