let G be Group; :: thesis: for f being Element of Aut G
for g being Element of (AutGroup G) st f = g holds
f " = g "
let f be Element of Aut G; :: thesis: for g being Element of (AutGroup G) st f = g holds
f " = g "
let g be Element of (AutGroup G); :: thesis: ( f = g implies f " = g " )
consider g1 being Element of Aut G such that
A1: g1 = g " ;
assume f = g ; :: thesis: f " = g "
then g1 * f = (g ") * g by A1, Def2;
then g1 * f = 1_ (AutGroup G) by GROUP_1:def 5;
then A2: g1 * f = id the carrier of G by Th9;
f is Homomorphism of G,G by Def1;
then A3: f is one-to-one by Def1;
rng f = dom f by Lm3
.= the carrier of G by Lm3 ;
hence f " = g " by A1, A3, A2, FUNCT_2:30; :: thesis: verum