:: deftheorem defines RAlgebra FUNCSDOM:def 8 :
for A being set holds RAlgebra A = AlgebraStr(# (Funcs (A,REAL)),(RealFuncMult A),(RealFuncAdd A),(RealFuncExtMult A),(RealFuncUnit A),(RealFuncZero A) #);