let p be Polynomial of F_Real; :: thesis: ( p is constant implies (Eval p) `| = REAL --> 0 )
assume p is constant ; :: thesis: (Eval p) `| = REAL --> 0
then ( p = 0_. F_Real or p = <%(p . 0)%> ) by Th23;
hence (Eval p) `| = REAL --> 0 by Th52, Lm2, Th11; :: thesis: verum