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