for A being with_empty-instruction Universal_Algebra
for o being Element of Operations A st o = Den ((In (1,(dom the charact of A))),A) holds
( arity o = 0 & EmptyIns A in rng o )