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 " )

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

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