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