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