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