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