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