set p = 1_. R;

assume 1_. R is with_roots ; :: thesis: contradiction

then consider x being Element of R such that

A: x is_a_root_of 1_. R by POLYNOM5:def 8;

0. R = eval ((1_. R),x) by A, POLYNOM5:def 7

.= 1. R by POLYNOM4:18 ;

hence contradiction ; :: thesis: verum

assume 1_. R is with_roots ; :: thesis: contradiction

then consider x being Element of R such that

A: x is_a_root_of 1_. R by POLYNOM5:def 8;

0. R = eval ((1_. R),x) by A, POLYNOM5:def 7

.= 1. R by POLYNOM4:18 ;

hence contradiction ; :: thesis: verum