let p1, p2 be Prime; :: thesis: for n1, n2 being Nat st ( n1 <> 0 or n2 <> 0 ) & p1 |^ n1 = p2 |^ n2 holds
( p1 = p2 & n1 = n2 )
let n1, n2 be Nat; :: thesis: ( ( n1 <> 0 or n2 <> 0 ) & p1 |^ n1 = p2 |^ n2 implies ( p1 = p2 & n1 = n2 ) )
assume that
AA: ( n1 <> 0 or n2 <> 0 ) and
AS: p1 |^ n1 = p2 |^ n2 ; :: thesis: ( p1 = p2 & n1 = n2 )

per cases ( ( n1 is zero & not n2 is zero ) or not n1 is zero ) by AA;

suppose that S1: n1 is zero and
S2: not n2 is zero ; :: thesis: ( p1 = p2 & n1 = n2 )

A1: p1 |^ n1 = 1 by S1, NEWTON:4;
p2 divides p2 |^ n2 by S2, NAT_3:3;
then p2 = 1 by AS, A1, INT_2:13;
hence ( p1 = p2 & n1 = n2 ) by INT_2:def 4; :: thesis: verum

end;

suppose not n1 is zero ; :: thesis: ( p1 = p2 & n1 = n2 )

then reconsider m = n1 - 1 as Nat ;
n1 = m + 1 ;
then p1 |^ n1 = (p1 |^ m) * p1 by NEWTON:6;
hence p1 = p2 by AS, NAT_D:def 3, NAT_3:6; :: thesis: n1 = n2
then ( n1 <= n2 & n2 <= n1 ) by AS, NAT_6:2;
hence n1 = n2 by XXREAL_0:1; :: thesis: verum

end;

end;