theorem lem1: :: RING_5:47

for n being even Nat
for x being Element of F_Real holds eval ((npoly (F_Real,n)),x) > 0. F_Real