let a, n be Nat; :: thesis: for p being prime Nat st a divides p |^ n holds
ex k being Nat st a = p |^ k
let p be prime Nat; :: thesis: ( a divides p |^ n implies ex k being Nat st a = p |^ k )
assume a divides p |^ n ; :: thesis: ex k being Nat st a = p |^ k
then ex k being Nat st
( a = p |^ k & k <= n ) by GROUPP_1:2;
hence ex k being Nat st a = p |^ k ; :: thesis: verum