let G be strict 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

( (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