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