let G be Group; :: thesis: for a being Element of G holds
( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )
let a be Element of G; :: thesis: ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )
Conjugate (1_ G) = id the carrier of G by Th22;
hence ( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a ) by FUNCT_2:17; :: thesis: verum