eval ((npoly (F_Real,n)),(- (1. F_Real))) = 0. F_Real by lem1c;
hence npoly (F_Real,n) is with_roots by POLYNOM5:def 8, POLYNOM5:def 7; :: thesis: verum