let G be strict Group; :: thesis: for f being Element of InnAut G

for g being Element of (InnAutGroup G) st f = g holds

f " = g "

let f be Element of InnAut G; :: thesis: for g being Element of (InnAutGroup G) st f = g holds

f " = g "

let g be Element of (InnAutGroup G); :: thesis: ( f = g implies f " = g " )

g is Element of (AutGroup G) by GROUP_2:42;

then consider g1 being Element of (AutGroup G) such that

A1: g1 = g ;

f is Element of Aut G by Th12;

then consider f1 being Element of Aut G such that

A2: f1 = f ;

assume f = g ; :: thesis: f " = g "

then f1 " = g1 " by A2, A1, Th10;

hence f " = g " by A2, A1, GROUP_2:48; :: thesis: verum

for g being Element of (InnAutGroup G) st f = g holds

f " = g "

let f be Element of InnAut G; :: thesis: for g being Element of (InnAutGroup G) st f = g holds

f " = g "

let g be Element of (InnAutGroup G); :: thesis: ( f = g implies f " = g " )

g is Element of (AutGroup G) by GROUP_2:42;

then consider g1 being Element of (AutGroup G) such that

A1: g1 = g ;

f is Element of Aut G by Th12;

then consider f1 being Element of Aut G such that

A2: f1 = f ;

assume f = g ; :: thesis: f " = g "

then f1 " = g1 " by A2, A1, Th10;

hence f " = g " by A2, A1, GROUP_2:48; :: thesis: verum