theorem :: ANPROJ_2:20

for A being non empty set
for x1, x2, x3, x4 being Element of A st A = {x1,x2,x3,x4} & 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 h9 being Element of Funcs (A,REAL) ex a, b, c, d being Real st h9 = (RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncAdd A) . (((RealFuncExtMult A) . [a,f]),((RealFuncExtMult A) . [b,g]))),((RealFuncExtMult A) . [c,h]))),((RealFuncExtMult A) . [d,f1]))