theorem :: FUNCSDOM:24

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