take p ; :: according to NUMBER08:def 6 :: thesis: ( p divides p |^ k & ( for r being Prime st r <> p holds
not r divides p |^ k ) )
thus p divides p |^ k by NAT_3:3; :: thesis: for r being Prime st r <> p holds
not r divides p |^ k
thus for r being Prime st r <> p holds
not r divides p |^ k by NAT_3:6; :: thesis: verum