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