let n be even Nat; :: thesis: for x being Element of F_Real holds eval ((npoly (F_Real,n)),x) > 0. F_Real
let x be Element of F_Real; :: thesis: eval ((npoly (F_Real,n)),x) > 0. F_Real

per cases ( n = 0 or not n is zero ) ;

suppose n = 0 ; :: thesis: eval ((npoly (F_Real,n)),x) > 0. F_Real

hence eval ((npoly (F_Real,n)),x) > 0. F_Real by lem1e; :: thesis: verum

end;

suppose S: not n is zero ; :: thesis: eval ((npoly (F_Real,n)),x) > 0. F_Real

(x |^ n) + 1 >= (0. F_Real) + 1 by XX, XREAL_1:6;
then (x |^ n) + (1. F_Real) >= 1 ;
hence eval ((npoly (F_Real,n)),x) > 0. F_Real by lem1a, S; :: thesis: verum

end;

end;