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 Th16
.= (((a ") * (1_ G)) * (b ")) * (a * b) by GROUP_1:def 4
.= (((a ") * (1_ G)) * (b ")) * ((a * (1_ G)) * b) by GROUP_1:def 4
.= (((a ") * ((a ") * a)) * (b ")) * ((a * (1_ G)) * b) by GROUP_1:def 5
.= (((a ") * ((a ") * a)) * (b ")) * ((a * ((b ") * b)) * b) by GROUP_1:def 5
.= ((((a ") * (a ")) * a) * (b ")) * ((a * ((b ") * b)) * b) by GROUP_1:def 3
.= ((((a ") |^ 2) * a) * (b ")) * ((a * ((b ") * b)) * b) by GROUP_1:27
.= ((((a ") |^ 2) * a) * (b ")) * (a * (((b ") * b) * b)) by GROUP_1:def 3
.= ((((a ") |^ 2) * a) * (b ")) * (a * ((b ") * (b * b))) by GROUP_1:def 3
.= ((((a ") |^ 2) * a) * (b ")) * (a * ((b ") * (b |^ 2))) by GROUP_1:27
.= (((a ") |^ 2) * (a * (b "))) * (a * ((b ") * (b |^ 2))) by GROUP_1:def 3
.= ((a ") |^ 2) * ((a * (b ")) * (a * ((b ") * (b |^ 2)))) by GROUP_1:def 3
.= ((a ") |^ 2) * ((a * (b ")) * ((a * (b ")) * (b |^ 2))) by GROUP_1:def 3
.= ((a ") |^ 2) * (((a * (b ")) * (a * (b "))) * (b |^ 2)) by GROUP_1:def 3
.= (((a ") |^ 2) * ((a * (b ")) * (a * (b ")))) * (b |^ 2) by GROUP_1:def 3
.= (((a ") |^ 2) * ((a * (b ")) |^ 2)) * (b |^ 2) by GROUP_1:27 ; :: thesis: verum