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

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

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

A7:
f is Element of Aut G
by Th12;
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;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

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