let G be strict Group; :: thesis: for f being Element of InnAut G holds

( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )

let f be Element of InnAut G; :: thesis: ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )

Conjugate (1_ G) = id the carrier of G by Th22;

hence ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) by FUNCT_2:17; :: thesis: verum

( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )

let f be Element of InnAut G; :: thesis: ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f )

Conjugate (1_ G) = id the carrier of G by Th22;

hence ( f * (Conjugate (1_ G)) = f & (Conjugate (1_ G)) * f = f ) by FUNCT_2:17; :: thesis: verum