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 4
.= a * ((a " ) * ((b " ) * (a * b))) by GROUP_1:def 4
.= (a * (a " )) * ((b " ) * (a * b)) by GROUP_1:def 4
.= (1_ G) * ((b " ) * (a * b)) by GROUP_1:def 6
.= (b " ) * (a * b) by GROUP_1:def 5
.= ((b " ) * a) * b by GROUP_1:def 4 ;
hence a |^ b = a * [.a,b.] ; :: thesis: verum