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 " )
assume A1: f = g ; :: thesis: f " = g "
f is Element of Aut G by Th13;
then consider f1 being Element of Aut G such that
A2: f1 = f ;
g is Element of (AutGroup G) by GROUP_2:51;
then consider g1 being Element of (AutGroup G) such that
A3: g1 = g ;
f1 " = g1 " by A1, A2, A3, Th11;
hence f " = g " by A2, A3, GROUP_2:57; :: thesis: verum