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

then f1 = id the carrier of G ;

hence f = 1_ (InnAutGroup G) by A2, Th19; :: thesis: verum

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

for x being Element of G holds f1 . x = (id the carrier of G) . x
by A4;
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;thus f1 . x = x |^ a by A3

.= x by A1, GROUP_3:29 ; :: thesis: verum

then f1 = id the carrier of G ;

hence f = 1_ (InnAutGroup G) by A2, Th19; :: thesis: verum