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

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