theorem Th74: :: POLYNOM5:74

for p being Polynomial of F_Complex st len p > 1 holds
p is with_roots