let G be Group; :: thesis: ( G is p -group & G is finite & G is commutative implies G is p -commutative-group )
assume A1: ( G is p -group & G is finite & G is commutative ) ; :: thesis: G is p -commutative-group
for a, b being Element of G holds (a * b) |^ p = (a |^ p) * (b |^ p) by A1, GROUP_1:48;
then G is p -commutative-group-like ;
hence G is p -commutative-group by A1; :: thesis: verum