let G be Group; :: thesis: for a, b being Element of G holds a |^ b = a * [.a,b.]
let a, b be Element of G; :: thesis: a |^ b = a * [.a,b.]
a * [.a,b.] = a * (((a ") * (b ")) * (a * b)) by GROUP_1:def 3
.= a * ((a ") * ((b ") * (a * b))) by GROUP_1:def 3
.= (a * (a ")) * ((b ") * (a * b)) by GROUP_1:def 3
.= (1_ G) * ((b ") * (a * b)) by GROUP_1:def 5
.= (b ") * (a * b) by GROUP_1:def 4
.= ((b ") * a) * b by GROUP_1:def 3 ;
hence a |^ b = a * [.a,b.] ; :: thesis: verum