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)) ") by XTUPLE_0:def 2
.= (0. L) * ((eval (((0._ L) `2),x)) ") by POLYNOM4:17
.= 0. L by VECTSP_1:7 ; :: thesis: verum