let q1, q, n1 be Element of NAT ; :: thesis: ( q1 divides q |^ n1 & q is prime & q1 is prime & n1 > 0 implies q = q1 )
assume A1: ( q1 divides q |^ n1 & q is prime ) ; :: thesis: ( not q1 is prime or not n1 > 0 or q = q1 )
assume A2: ( q1 is prime & n1 > 0 ) ; :: thesis: q = q1
then q1 > 1 by INT_2:def 5;
then consider k being Element of NAT such that
A4: q1 = q * k by A1, PEPIN:33;
k divides q1 by A4, NAT_D:def 3;
then A5: ( k = 1 or k = q1 ) by A2, INT_2:def 5;
k <> q1

proof

assume k = q1 ; :: thesis: contradiction
then q = 1 by A2, A4, XCMPLX_1:7;
hence contradiction by A1, INT_2:def 5; :: thesis: verum

end;

hence q = q1 by A4, A5; :: thesis: verum