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