let G be Group; :: thesis: for a, b, g being Element of G holds (a * b) |^ g = (a |^ g) * (b |^ g)
let a, b, g be Element of G; :: thesis: (a * b) |^ g = (a |^ g) * (b |^ g)
thus (a * b) |^ g = ((g ") * ((a * (1_ G)) * b)) * g by GROUP_1:def 4
.= ((g ") * ((a * (g * (g "))) * b)) * g by GROUP_1:def 5
.= ((g ") * (((a * g) * (g ")) * b)) * g by GROUP_1:def 3
.= ((g ") * ((a * g) * ((g ") * b))) * g by GROUP_1:def 3
.= (((g ") * (a * g)) * ((g ") * b)) * g by GROUP_1:def 3
.= ((a |^ g) * ((g ") * b)) * g by GROUP_1:def 3
.= (a |^ g) * (b |^ g) by GROUP_1:def 3 ; :: thesis: verum