set q = npoly (F_Real,n);

now :: thesis: not npoly (F_Real,n) is with_roots

hence
not npoly (F_Real,n) is with_roots
; :: thesis: verumassume
npoly (F_Real,n) is with_roots
; :: thesis: contradiction

then consider r being Element of F_Real such that

H: r is_a_root_of npoly (F_Real,n) by POLYNOM5:def 8;

eval ((npoly (F_Real,n)),r) = 0. F_Real by H, POLYNOM5:def 7;

hence contradiction by lem1; :: thesis: verum

end;then consider r being Element of F_Real such that

H: r is_a_root_of npoly (F_Real,n) by POLYNOM5:def 8;

eval ((npoly (F_Real,n)),r) = 0. F_Real by H, POLYNOM5:def 7;

hence contradiction by lem1; :: thesis: verum