let G be strict 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 " )
assume A1: f = g ; :: thesis: f " = g "
consider g1 being Element of Aut G such that
A2: g1 = g " ;
A3: rng f = dom f by Lm3
.= the carrier of G by Lm3 ;
f is Homomorphism of G,G by Def1;
then A4: f is one-to-one by Def1;
g1 * f = (g " ) * g by A1, A2, Def2;
then g1 * f = 1_ (AutGroup G) by GROUP_1:def 6;
then g1 * f = id the carrier of G by Th10;
hence f " = g " by A2, A3, A4, FUNCT_2:36; :: thesis: verum