let p be Prime; :: thesis: support (pfexp p) = {p}
p = p |^ 1 ;
hence support (pfexp p) = {p} by Th42; :: thesis: verum