let G be strict Group; :: thesis: ( G is commutative Group implies for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G) )
assume A1: G is commutative Group ; :: thesis: for f being Element of (InnAutGroup G) holds f = 1_ (InnAutGroup G)
let f be Element of (InnAutGroup G); :: thesis: f = 1_ (InnAutGroup G)
the carrier of (InnAutGroup G) = InnAut G by Def5;
then consider f1 being Element of InnAut G such that
A2: f1 = f ;
f1 is Element of Funcs ( the carrier of G, the carrier of G) by FUNCT_2:8;
then consider a being Element of G such that
A3: for x being Element of G holds f1 . x = x |^ a by Def4;
A4: for x being Element of G holds f1 . x = x
proof
let x be Element of G; :: thesis: f1 . x = x
thus f1 . x = x |^ a by A3
.= x by A1, GROUP_3:29 ; :: thesis: verum
end;
for x being Element of G holds f1 . x = (id the carrier of G) . x by A4;
then f1 = id the carrier of G ;
hence f = 1_ (InnAutGroup G) by A2, Th19; :: thesis: verum