let G be strict Group; :: thesis: for f being Element of InnAut G holds f is Element of Aut G
let f be Element of InnAut G; :: thesis: f is Element of Aut G
A1: f is Element of Funcs the carrier of G,the carrier of G by FUNCT_2:12;

now

let x, y be Element of G; :: thesis: f . (x * y) = (f . x) * (f . y)
consider a being Element of G such that
A2: for x being Element of G holds f . x = x |^ a by A1, Def4;
thus f . (x * y) = (x * y) |^ a by A2
.= (((a " ) * x) * y) * a by GROUP_1:def 4
.= ((a " ) * x) * (y * a) by GROUP_1:def 4
.= (((a " ) * x) * (1_ G)) * (y * a) by GROUP_1:def 5
.= (((a " ) * x) * (a * (a " ))) * (y * a) by GROUP_1:def 6
.= ((((a " ) * x) * a) * (a " )) * (y * a) by GROUP_1:def 4
.= (((((a " ) * x) * a) * (a " )) * y) * a by GROUP_1:def 4
.= ((((a " ) * x) * a) * ((a " ) * y)) * a by GROUP_1:def 4
.= (x |^ a) * (y |^ a) by GROUP_1:def 4
.= (f . x) * (y |^ a) by A2
.= (f . x) * (f . y) by A2 ; :: thesis: verum

end;

then reconsider f = f as Homomorphism of G,G by GROUP_6:def 7;
A3: f is one-to-one

proof

let q be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not q in proj1 f or not b₁ in proj1 f or not f . q = f . b₁ or q = b₁ )
let q1 be set ; :: thesis: ( not q in proj1 f or not q1 in proj1 f or not f . q = f . q1 or q = q1 )
assume that
A4: ( q in dom f & q1 in dom f ) and
A5: f . q = f . q1 ; :: thesis: q = q1
consider x, y being Element of G such that
A6: ( x = q & y = q1 ) by A4;
consider a being Element of G such that
A7: for x being Element of G holds f . x = x |^ a by A1, Def4;
f . x = y |^ a by A7, A5, A6;
then x |^ a = y |^ a by A7;
then a * ((a " ) * (x * a)) = a * (((a " ) * y) * a) by GROUP_1:def 4;
then (a * (a " )) * (x * a) = a * (((a " ) * y) * a) by GROUP_1:def 4;
then (a * (a " )) * (x * a) = a * ((a " ) * (y * a)) by GROUP_1:def 4;
then (a * (a " )) * (x * a) = (a * (a " )) * (y * a) by GROUP_1:def 4;
then (1_ G) * (x * a) = (a * (a " )) * (y * a) by GROUP_1:def 6;
then (1_ G) * (x * a) = (1_ G) * (y * a) by GROUP_1:def 6;
then x * a = (1_ G) * (y * a) by GROUP_1:def 5;
then (x * a) * (a " ) = (y * a) * (a " ) by GROUP_1:def 5;
then x * (a * (a " )) = (y * a) * (a " ) by GROUP_1:def 4;
then x * (a * (a " )) = y * (a * (a " )) by GROUP_1:def 4;
then x * (1_ G) = y * (a * (a " )) by GROUP_1:def 6;
then x * (1_ G) = y * (1_ G) by GROUP_1:def 6;
then x = y * (1_ G) by GROUP_1:def 5;
hence q = q1 by A6, GROUP_1:def 5; :: thesis: verum

end;

for q being set st q in the carrier of G holds
ex q1 being set st
( q1 in dom f & q = f . q1 )

proof

let q be set ; :: thesis: ( q in the carrier of G implies ex q1 being set st
( q1 in dom f & q = f . q1 ) )
assume q in the carrier of G ; :: thesis: ex q1 being set st
( q1 in dom f & q = f . q1 )
then consider y being Element of G such that
A8: y = q ;
consider a being Element of G such that
A9: for x being Element of G holds f . x = x |^ a by A1, Def4;
take q1 = (a * y) * (a " ); :: thesis: ( q1 in dom f & q = f . q1 )
ex f1 being Function st
( f = f1 & dom f1 = the carrier of G & rng f1 c= the carrier of G ) by A1, FUNCT_2:def 2;
hence q1 in dom f ; :: thesis: q = f . q1
y = (1_ G) * y by GROUP_1:def 5
.= ((1_ G) * y) * (1_ G) by GROUP_1:def 5
.= (((a " ) * a) * y) * (1_ G) by GROUP_1:def 6
.= (((a " ) * a) * y) * ((a " ) * a) by GROUP_1:def 6
.= ((((a " ) * a) * y) * (a " )) * a by GROUP_1:def 4
.= (((a " ) * a) * (y * (a " ))) * a by GROUP_1:def 4
.= ((a " ) * (a * (y * (a " )))) * a by GROUP_1:def 4
.= q1 |^ a by GROUP_1:def 4
.= f . q1 by A9 ;
hence q = f . q1 by A8; :: thesis: verum

end;

then the carrier of G c= rng f by FUNCT_1:19;
then rng f = the carrier of G by XBOOLE_0:def 10;
then f is onto by FUNCT_2:def 3;
hence f is Element of Aut G by A3, Def1; :: thesis: verum