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