let G be strict Group; :: thesis: for f being Element of InnAut G holds f " is Element of InnAut G
let f be Element of InnAut G; :: thesis: f " is Element of InnAut G
reconsider f1 = f as Element of Funcs the carrier of G,the carrier of G by FUNCT_2:12;
f1 = f ;
then consider f1 being Element of Funcs the carrier of G,the carrier of G such that
A1: f1 = f ;
A2: f is Element of Aut G by Th13;
then reconsider f2 = f as Homomorphism of G,G by Def1;
f2 = f ;
then consider f2 being Homomorphism of G,G such that
A3: f2 = f ;
( f2 is one-to-one & f2 is onto ) by A2, A3, Def1;
then ( f2 is one-to-one & rng f2 = the carrier of G ) by FUNCT_2:def 3;
then f " is Function of the carrier of G,the carrier of G by A3, FUNCT_2:31;
then A4: f " is Element of Funcs the carrier of G,the carrier of G by FUNCT_2:12;
ex a being Element of G st
for x being Element of G holds (f " ) . x = x |^ a

proof

consider b being Element of G such that
A5: for y being Element of G holds f1 . y = y |^ b by A1, Def4;
take a = b " ; :: thesis: for x being Element of G holds (f " ) . x = x |^ a
let x be Element of G; :: thesis: (f " ) . x = x |^ a
A6: f1 is Element of Aut G by A1, Th13;
then reconsider f1 = f1 as Homomorphism of G,G by Def1;
f1 is bijective by A6, Th5;
then A7: ( f1 is onto & f1 is one-to-one ) ;
then consider y1 being Element of G such that
A8: x = f1 . y1 by GROUP_6:68;
f1 is one-to-one by A7;
then (f1 " ) . x = y1 by A8, FUNCT_2:32
.= (1_ G) * y1 by GROUP_1:def 5
.= ((1_ G) * y1) * (1_ G) by GROUP_1:def 5
.= ((b * (b " )) * y1) * (1_ G) by GROUP_1:def 6
.= ((b * (b " )) * y1) * (b * (b " )) by GROUP_1:def 6
.= (((b * (b " )) * y1) * b) * (b " ) by GROUP_1:def 4
.= ((b * (b " )) * (y1 * b)) * (b " ) by GROUP_1:def 4
.= (b * ((b " ) * (y1 * b))) * (b " ) by GROUP_1:def 4
.= (b * (y1 |^ b)) * (b " ) by GROUP_1:def 4
.= (b * x) * (b " ) by A5, A8
.= ((a " ) * x) * a by GROUP_1:19 ;
hence (f " ) . x = x |^ a by A1; :: thesis: verum

end;

hence f " is Element of InnAut G by A4, Def4; :: thesis: verum