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 Th19
.= (1_ G) * (a * (a " )) by GROUP_1:def 6
.= a * (a " ) by GROUP_1:def 5
.= 1_ G by GROUP_1:def 6 ; :: thesis: [.(a " ),a.] = 1_ G
thus [.(a " ),a.] = (((a " ) " ) * (a " )) * ((a " ) * a) by Th19
.= (((a " ) " ) * (a " )) * (1_ G) by GROUP_1:def 6
.= ((a " ) " ) * (a " ) by GROUP_1:def 5
.= 1_ G by GROUP_1:def 6 ; :: thesis: verum