let n be odd Nat; :: thesis: eval ((npoly (F_Real,n)),(- (1. F_Real))) = 0. F_Real
consider k being Nat such that
H: n - 1 = 2 * k by ABIAN:def 2;
A: k is Element of NAT by ORDINAL1:def 12;
(- (1. F_Real)) |^ n = (power F_Real) . ((- (1. F_Real)),((2 * k) + 1)) by H
.= - (1_ F_Real) by A, HURWITZ:4
.= - (1. F_Real) ;
hence eval ((npoly (F_Real,n)),(- (1. F_Real))) = (- (1. F_Real)) + (1. F_Real) by lem1a
.= 0. F_Real ;
:: thesis: verum