theorem Th20: :: FUNCSDOM:20

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