let G be Group; for a, b being Element of G holds
( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
let a, b be Element of G; ( [.a,b.] = (((a ") * (b ")) * a) * b & [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
thus
[.a,b.] = (((a ") * (b ")) * a) * b
; ( [.a,b.] = ((a ") * ((b ") * a)) * b & [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
thus
[.a,b.] = ((a ") * ((b ") * a)) * b
by GROUP_1:def 3; ( [.a,b.] = (a ") * (((b ") * a) * b) & [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
hence
[.a,b.] = (a ") * (((b ") * a) * b)
by GROUP_1:def 3; ( [.a,b.] = (a ") * ((b ") * (a * b)) & [.a,b.] = ((a ") * (b ")) * (a * b) )
hence
[.a,b.] = (a ") * ((b ") * (a * b))
by GROUP_1:def 3; [.a,b.] = ((a ") * (b ")) * (a * b)
thus
[.a,b.] = ((a ") * (b ")) * (a * b)
by GROUP_1:def 3; verum