theorem :: ANPROJ_2:12

for A being non empty set
for x1, x2, x3 being Element of A st x1 <> x2 & x1 <> x3 & x2 <> x3 holds
ex f, g, h being Element of Funcs (A,REAL) st
for a, b, c being Real st (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h])) = RealFuncZero A holds
( a = 0 & b = 0 & c = 0 )