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 5
.= ((g ") * ((a * (g * (g "))) * b)) * g by GROUP_1:def 6
.= ((g ") * (((a * g) * (g ")) * b)) * g by GROUP_1:def 4
.= ((g ") * ((a * g) * ((g ") * b))) * g by GROUP_1:def 4
.= (((g ") * (a * g)) * ((g ") * b)) * g by GROUP_1:def 4
.= ((a |^ g) * ((g ") * b)) * g by GROUP_1:def 4
.= (a |^ g) * (b |^ g) by GROUP_1:def 4 ; :: thesis: verum