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 Th27

.= ([.a,b.] |^ (b ")) |^ (a ") by Th27

.= [.a,b.] |^ ((b ") * (a ")) by GROUP_3:24

.= [.a,b.] |^ ((a * b) ") by GROUP_1:17 ; :: thesis: [.(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 ; :: thesis: verum

( [.(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 Th27

.= ([.a,b.] |^ (b ")) |^ (a ") by Th27

.= [.a,b.] |^ ((b ") * (a ")) by GROUP_3:24

.= [.a,b.] |^ ((a * b) ") by GROUP_1:17 ; :: thesis: [.(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 ; :: thesis: verum