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:9;
f1 = f ;
then consider f1 being Element of Funcs ( the carrier of G, the carrier of G) such that
A1: f1 = f ;
A2: 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
A3: 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
A4: f1 is Element of Aut G by A1, Th12;
then reconsider f1 = f1 as Homomorphism of G,G by Def1;
A5: f1 is bijective by A4, Th4;
then consider y1 being Element of G such that
A6: x = f1 . y1 by GROUP_6:58;
(f1 ") . x = y1 by A5, A6, FUNCT_2:26
.= (1_ G) * y1 by GROUP_1:def 4
.= ((1_ G) * y1) * (1_ G) by GROUP_1:def 4
.= ((b * (b ")) * y1) * (1_ G) by GROUP_1:def 5
.= ((b * (b ")) * y1) * (b * (b ")) by GROUP_1:def 5
.= (((b * (b ")) * y1) * b) * (b ") by GROUP_1:def 3
.= ((b * (b ")) * (y1 * b)) * (b ") by GROUP_1:def 3
.= (b * ((b ") * (y1 * b))) * (b ") by GROUP_1:def 3
.= (b * (y1 |^ b)) * (b ") by GROUP_1:def 3
.= (b * x) * (b ") by A3, A6
.= ((a ") * x) * a ;
hence (f ") . x = x |^ a by A1; :: thesis: verum
end;
A7: f is Element of Aut G by Th12;
then reconsider f2 = f as Homomorphism of G,G by Def1;
f2 = f ;
then consider f2 being Homomorphism of G,G such that
A8: f2 = f ;
f2 is onto by A7, A8, Def1;
then A9: rng f2 = the carrier of G ;
f2 is one-to-one by A7, A8, Def1;
then f " is Function of the carrier of G, the carrier of G by A8, A9, FUNCT_2:25;
then f " is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:9;
hence f " is Element of InnAut G by A2, Def4; :: thesis: verum