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:50; :: thesis: verum