let L be Field; :: thesis: for x being Element of L holds eval ((0._ L),x) = 0. L
let x be Element of L; :: thesis: eval ((0._ L),x) = 0. L
thus eval ((0._ L),x) = (eval ((0_. L),x)) * ((eval (((0._ L) `2),x)) ")
.= (0. L) * ((eval (((0._ L) `2),x)) ") by POLYNOM4:17
.= 0. L ; :: thesis: verum