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