let G be strict Group; :: thesis: for a being Element of G holds (Conjugate (1_ G)) . a = a
let a be Element of G; :: thesis: (Conjugate (1_ G)) . a = a
thus (Conjugate (1_ G)) . a = a |^ (1_ G) by Def6
.= a by GROUP_3:19 ; :: thesis: verum