theorem :: FUNCSDOM:27

for A being non empty set holds 1. (RAlgebra A) = RealFuncUnit A ;