let a, b be Nat; :: thesis: ( card G = p |^ a & card G = p |^ b implies a = b )
assume that
A3: card G = p |^ a and
A4: card G = p |^ b ; :: thesis: a = b
p > 1 by INT_2:def 5;
hence a = b by A3, A4, PEPIN:31; :: thesis: verum