theorem Th18: :: FUNCSDOM:18

for x1, x2 being set
for A being non empty set
for f, g being Element of Funcs (A,REAL) st x1 in A & x2 in A & x1 <> x2 & f = (RealFuncZero A) +* (x1 .--> 1) & g = (RealFuncUnit A) +* (x1 .--> 0) holds
for a, b being Real st (RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g])) = RealFuncZero A holds
( a = 0 & b = 0 )