theorem :: AUTALG_1:7

for UA being Universal_Algebra
for x, y being Element of (UAAutGroup UA)
for f, g being Element of UAAut UA st x = f & y = g holds
x * y = g * f by Def2;