:: deftheorem defines Four0 POLYEQ_2:def 2 :
for a1, x1, x2, x3, x4, x being Real holds Four0 (a1,x1,x2,x3,x4,x) = a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4));