let G be Group; :: thesis: for a being Element of G
for f being Endomorphism of G st a is_inner_wrt f holds
f is Automorphism of G
let a be Element of G; :: thesis: for f being Endomorphism of G st a is_inner_wrt f holds
f is Automorphism of G
let f be Endomorphism of G; :: thesis: ( a is_inner_wrt f implies f is Automorphism of G )
assume A1: a is_inner_wrt f ; :: thesis: f is Automorphism of G
then Ker f = (1). G by Th29;
then A2: f is one-to-one by GROUP_6:56;
ex fInv being Endomorphism of G st f * fInv = id the carrier of G

proof

deffunc H₁( Element of G) -> Element of the carrier of G = $1 |^ (a ");
consider fInv being Function of the carrier of G, the carrier of G such that
A3: for g being Element of G holds fInv . g = H₁(g) from FUNCT_2:sch 4();
for x1, x2 being Element of G holds fInv . (x1 * x2) = (fInv . x1) * (fInv . x2)

proof

let x1, x2 be Element of G; :: thesis: fInv . (x1 * x2) = (fInv . x1) * (fInv . x2)
A4: ( fInv . x1 = x1 |^ (a ") & fInv . x2 = x2 |^ (a ") ) by A3;
fInv . (x1 * x2) = (x1 * x2) |^ (a ") by A3
.= (x1 |^ (a ")) * (x2 |^ (a ")) by GROUP_3:23
.= (fInv . x1) * (fInv . x2) by A4 ;
hence fInv . (x1 * x2) = (fInv . x1) * (fInv . x2) ; :: thesis: verum

end;

then reconsider fInv = fInv as Endomorphism of G by GROUP_6:def 6;
for x being Element of G holds (f * fInv) . x = (id the carrier of G) . x

proof

let x be Element of G; :: thesis: (f * fInv) . x = (id the carrier of G) . x
(f * fInv) . x = f . (fInv . x) by FUNCT_2:15
.= f . (x |^ (a ")) by A3
.= (x |^ (a ")) |^ a by A1
.= x |^ ((a ") * a) by GROUP_3:24
.= x |^ (1_ G) by GROUP_1:def 5
.= x by GROUP_3:19
.= (id the carrier of G) . x ;
hence (f * fInv) . x = (id the carrier of G) . x ; :: thesis: verum

end;

then f * fInv = id the carrier of G ;
hence ex fInv being Endomorphism of G st f * fInv = id the carrier of G ; :: thesis: verum

end;

then f is onto by FUNCT_2:18;
hence f is Automorphism of G by A2; :: thesis: verum