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
len p > 0 by Th19;
then A2: (len (poly_quotient p,r)) + 1 = len p by A1, Def7;
assume len (poly_quotient p,r) <= 0 ; :: thesis: contradiction
then len (poly_quotient p,r) = 0 ;
then Roots p = {} by A2, Th48;
hence contradiction by A1, POLYNOM5:def 9; :: thesis: verum