let G be Group; :: thesis: for a, b, c being Element of G holds ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G
let a, b, c be Element of G; :: thesis: ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G
( [.a,b,(c |^ a).] = [.b,(a "),c.] |^ a & [.c,a,(b |^ c).] = [.a,(c "),b.] |^ c & [.b,c,(a |^ b).] = [.c,(b "),a.] |^ b ) by Th7;
hence ([.a,b,(c |^ a).] * [.c,a,(b |^ c).]) * [.b,c,(a |^ b).] = 1_ G by GROUP_5:46; :: thesis: verum