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