theorem
for
A being non
empty set for
x1,
x2,
x3,
x4 being
Element of
A st
x1 <> x2 &
x1 <> x3 &
x1 <> x4 &
x2 <> x3 &
x2 <> x4 &
x3 <> x4 holds
ex
f,
g,
h,
f1 being
Element of
Funcs (
A,
REAL) st
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 )