let L be non degenerated comRing; :: thesis: 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; :: thesis: 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; :: thesis: ( r is_a_root_of p implies len (poly_quotient (p,r)) > 0 )

assume A1: r is_a_root_of p ; :: thesis: len (poly_quotient (p,r)) > 0

assume len (poly_quotient (p,r)) <= 0 ; :: thesis: 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; :: thesis: verum

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; :: thesis: 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; :: thesis: ( r is_a_root_of p implies len (poly_quotient (p,r)) > 0 )

assume A1: r is_a_root_of p ; :: thesis: len (poly_quotient (p,r)) > 0

assume len (poly_quotient (p,r)) <= 0 ; :: thesis: 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; :: thesis: verum