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