:: deftheorem defines RRing FUNCSDOM:def 7 :
for A being non empty set holds RRing A = doubleLoopStr(# (Funcs (A,REAL)),(RealFuncAdd A),(RealFuncMult A),(RealFuncUnit A),(RealFuncZero A) #);