let G be Group; :: thesis: for a being Element of G holds
( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )
let a be Element of G; :: thesis: ( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )
thus [.a,(a ").] = ((a ") * ((a ") ")) * (a * (a ")) by Th16
.= (1_ G) * (a * (a ")) by GROUP_1:def 5
.= a * (a ") by GROUP_1:def 4
.= 1_ G by GROUP_1:def 5 ; :: thesis: [.(a "),a.] = 1_ G
thus [.(a "),a.] = (((a ") ") * (a ")) * ((a ") * a) by Th16
.= (((a ") ") * (a ")) * (1_ G) by GROUP_1:def 5
.= ((a ") ") * (a ") by GROUP_1:def 4
.= 1_ G by GROUP_1:def 5 ; :: thesis: verum