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