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:96;
then G is p -commutative-group-like by def3;
hence G is p -commutative-group by a1; :: thesis: verum