let G be Group; :: thesis: for p being prime Nat holds (1). G is p -commutative-group-like
let p be prime Nat; :: thesis: (1). G is p -commutative-group-like
let a, b be Element of ((1). G); :: according to GROUPP_1:def 3 :: thesis: (a * b) |^ p = (a |^ p) * (b |^ p)
A1: the carrier of ((1). G) = {(1_ G)} by GROUP_2:def 7;
hence (a * b) |^ p = 1_ G by TARSKI:def 1
.= (a |^ p) * (b |^ p) by A1, TARSKI:def 1 ;
:: thesis: verum