let G be Group; :: thesis: 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; :: thesis: ( [.(a "),(b ").] = [.a,b.] |^ ((a * b) ") & [.(a "),(b ").] = [.a,b.] |^ ((b * a) ") )
thus [.(a "),(b ").] = [.(b "),a.] |^ (a ") by Th30
.= ([.a,b.] |^ (b ")) |^ (a ") by Th30
.= [.a,b.] |^ ((b ") * (a ")) by GROUP_3:29
.= [.a,b.] |^ ((a * b) ") by GROUP_1:25 ; :: thesis: [.(a "),(b ").] = [.a,b.] |^ ((b * a) ")
thus [.(a "),(b ").] = [.b,(a ").] |^ (b ") by Th31
.= ([.a,b.] |^ (a ")) |^ (b ") by Th31
.= [.a,b.] |^ ((a ") * (b ")) by GROUP_3:29
.= [.a,b.] |^ ((b * a) ") by GROUP_1:25 ; :: thesis: verum