:: deftheorem defines Operations UNIALG_2:def 2 :
for U0 being Universal_Algebra holds Operations U0 = rng the charact of U0;