let L be non degenerated comRing; for r being Element of L
for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0
let r be Element of L; for p being non-zero Polynomial of L st r is_a_root_of p holds
len (poly_quotient (p,r)) > 0
let p be non-zero Polynomial of L; ( r is_a_root_of p implies len (poly_quotient (p,r)) > 0 )
assume A1:
r is_a_root_of p
; len (poly_quotient (p,r)) > 0
assume
len (poly_quotient (p,r)) <= 0
; contradiction
then A2:
len (poly_quotient (p,r)) = 0
;
len p > 0
by Th14;
then
(len (poly_quotient (p,r))) + 1 = len p
by A1, Def6;
then
Roots p = {}
by A2, Th43;
hence
contradiction
by A1, POLYNOM5:def 10; verum