let b be natural number ; :: thesis: for p, a being Prime st a divides p |^ b holds
a = p
let p, a be Prime; :: thesis: ( a divides p |^ b implies a = p )
assume A1: a divides p |^ b ; :: thesis: a = p
A2: a <> 1 by INT_2:def 5;
a divides p by A1, Th5;
hence a = p by A2, INT_2:def 5; :: thesis: verum