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

proof

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

end;

k divides q1 by A4, NAT_D:def 3;
then ( k = 1 or k = q1 ) by A3, INT_2:def 4;
hence q = q1 by A4, A5; :: thesis: verum