theorem Th17: :: ANPROJ_2:17

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