let UA be Universal_Algebra; :: thesis: id the carrier of UA = 1_ (UAAutGroup UA)
reconsider g = id the carrier of UA as Element of (UAAutGroup UA) by Th4;
consider g1 being Function of the carrier of UA,the carrier of UA such that
A1: g1 = g ;
consider f being Element of (UAAutGroup UA);
f is Element of UAAut UA ;
then consider f1 being Function of the carrier of UA,the carrier of UA such that
A2: f1 = f ;
g * f = f1 * g1 by A1, A2, Def2
.= f by A1, A2, FUNCT_2:23 ;
hence id the carrier of UA = 1_ (UAAutGroup UA) by GROUP_1:15; :: thesis: verum