for UA being Universal_Algebra
for f being Element of UAAut UA holds f " in UAAut UA