theorem Th17: :: FUNCSDOM:17

for x1 being set
for A being non empty set st x1 in A holds
( (RealFuncZero A) +* (x1 .--> 1) in Funcs (A,REAL) & (RealFuncUnit A) +* (x1 .--> 0) in Funcs (A,REAL) )