for A being set
for f being Element of Funcs (A,REAL) holds (RealFuncAdd A) . (f,((RealFuncExtMult A) . [(- 1),f])) = RealFuncZero A