let G be Group; for a, b being Element of G holds
( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
let a, b be Element of G; ( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
thus [.(a "),(b ").] =
[.(b "),a.] |^ (a ")
by Th27
.=
([.a,b.] |^ (b ")) |^ (a ")
by Th27
.=
[.a,b.] |^ ((b ") * (a "))
by GROUP_3:24
.=
[.a,b.] |^ ((a * b) ")
by GROUP_1:17
; [.(a "),(b ").] = [.a,b.] |^ ((b * a) ")
thus [.(a "),(b ").] =
[.b,(a ").] |^ (b ")
by Th28
.=
([.a,b.] |^ (a ")) |^ (b ")
by Th28
.=
[.a,b.] |^ ((a ") * (b "))
by GROUP_3:24
.=
[.a,b.] |^ ((b * a) ")
by GROUP_1:17
; verum