theorem lem1c: :: RING_5:48
for n being odd Nat holds eval ((npoly (F_Real,n)),(- (1. F_Real))) = 0. F_Real