let G be 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:9;

now :: thesis: for x, y being Element of G holds f . (x * y) = (f . x) * (f . y)

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 3
.= ((a ") * x) * (y * a) by GROUP_1:def 3
.= (((a ") * x) * (1_ G)) * (y * a) by GROUP_1:def 4
.= (((a ") * x) * (a * (a "))) * (y * a) by GROUP_1:def 5
.= ((((a ") * x) * a) * (a ")) * (y * a) by GROUP_1:def 3
.= (((((a ") * x) * a) * (a ")) * y) * a by GROUP_1:def 3
.= ((((a ") * x) * a) * ((a ") * y)) * a by GROUP_1:def 3
.= (x |^ a) * (y |^ a) by GROUP_1:def 3
.= (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 6;
A3: f is one-to-one

proof

let q, q1 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not q in dom f or not q1 in dom 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 3;
then (a * (a ")) * (x * a) = a * (((a ") * y) * a) by GROUP_1:def 3;
then (a * (a ")) * (x * a) = a * ((a ") * (y * a)) by GROUP_1:def 3;
then (a * (a ")) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def 3;
then (1_ G) * (x * a) = (a * (a ")) * (y * a) by GROUP_1:def 5;
then (1_ G) * (x * a) = (1_ G) * (y * a) by GROUP_1:def 5;
then x * a = (1_ G) * (y * a) by GROUP_1:def 4;
then (x * a) * (a ") = (y * a) * (a ") by GROUP_1:def 4;
then x * (a * (a ")) = (y * a) * (a ") by GROUP_1:def 3;
then x * (a * (a ")) = y * (a * (a ")) by GROUP_1:def 3;
then x * (1_ G) = y * (a * (a ")) by GROUP_1:def 5;
then x * (1_ G) = y * (1_ G) by GROUP_1:def 5;
then x = y * (1_ G) by GROUP_1:def 4;
hence q = q1 by A6, GROUP_1:def 4; :: thesis: verum

end;

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

proof

let q be object ; :: thesis: ( q in the carrier of G implies ex q1 being object st
( q1 in dom f & q = f . q1 ) )
assume q in the carrier of G ; :: thesis: ex q1 being object 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 4
.= ((1_ G) * y) * (1_ G) by GROUP_1:def 4
.= (((a ") * a) * y) * (1_ G) by GROUP_1:def 5
.= (((a ") * a) * y) * ((a ") * a) by GROUP_1:def 5
.= ((((a ") * a) * y) * (a ")) * a by GROUP_1:def 3
.= (((a ") * a) * (y * (a "))) * a by GROUP_1:def 3
.= ((a ") * (a * (y * (a ")))) * a by GROUP_1:def 3
.= q1 |^ a by GROUP_1:def 3
.= f . q1 by A9 ;
hence q = f . q1 by A8; :: thesis: verum

end;

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