:: deftheorem Def3 defines oper FREEALG:def 3 :
for U1 being Universal_Algebra
for n being Nat st n in dom the charact of U1 holds
oper (n,U1) = the charact of U1 . n;