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