theorem Th54: :: POLYDIFF:54

for p being Polynomial of F_Real st p is constant holds
(Eval p) `| = REAL --> 0