let G be Group; :: thesis: for a, b, c being Element of G holds [.a,(b "),c.] |^ b = [.b,a,(c |^ b).]
let a, b, c be Element of G; :: thesis: [.a,(b "),c.] |^ b = [.b,a,(c |^ b).]
[.a,(b "),c.] |^ b = [.([.a,(b ").] |^ b),(c |^ b).] by Th5;
hence [.a,(b "),c.] |^ b = [.b,a,(c |^ b).] by Th6; :: thesis: verum