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