let UA be Universal_Algebra; :: thesis: for f being Element of UAAut UA

for g being Element of (UAAutGroup UA) st f = g holds

f " = g "

let f be Element of UAAut UA; :: thesis: for g being Element of (UAAutGroup UA) st f = g holds

f " = g "

let g be Element of (UAAutGroup UA); :: thesis: ( f = g implies f " = g " )

consider g1 being Element of UAAut UA such that

A1: g1 = g " ;

assume f = g ; :: thesis: f " = g "

then g1 * f = g * (g ") by A1, Def2;

then g1 * f = 1_ (UAAutGroup UA) by GROUP_1:def 5;

then A2: g1 * f = id the carrier of UA by Th8;

f is_isomorphism by Def1;

then f is_monomorphism ;

then A3: f is one-to-one ;

rng f = dom f by Lm2

.= the carrier of UA by Lm2 ;

hence f " = g " by A1, A3, A2, FUNCT_2:30; :: thesis: verum

for g being Element of (UAAutGroup UA) st f = g holds

f " = g "

let f be Element of UAAut UA; :: thesis: for g being Element of (UAAutGroup UA) st f = g holds

f " = g "

let g be Element of (UAAutGroup UA); :: thesis: ( f = g implies f " = g " )

consider g1 being Element of UAAut UA such that

A1: g1 = g " ;

assume f = g ; :: thesis: f " = g "

then g1 * f = g * (g ") by A1, Def2;

then g1 * f = 1_ (UAAutGroup UA) by GROUP_1:def 5;

then A2: g1 * f = id the carrier of UA by Th8;

f is_isomorphism by Def1;

then f is_monomorphism ;

then A3: f is one-to-one ;

rng f = dom f by Lm2

.= the carrier of UA by Lm2 ;

hence f " = g " by A1, A3, A2, FUNCT_2:30; :: thesis: verum