theorem :: ENDALG:5
for UA being Universal_Algebra holds id the carrier of UA = 1_ (UAEndMonoid UA) by Def3;