let L be Field; :: thesis: for x being Element of L holds eval ((1._ L),x) = 1. L
let x be Element of L; :: thesis: eval ((1._ L),x) = 1. L
A1: 1. L <> 0. L ;
thus eval ((1._ L),x) = (eval ((1_. L),x)) * ((eval (((1._ L) `2),x)) ")
.= (1. L) * ((eval (((1._ L) `2),x)) ") by POLYNOM4:18
.= (1. L) * ((eval ((1_. L),x)) ")
.= (1. L) * ((1. L) ") by POLYNOM4:18
.= 1. L by A1, VECTSP_1:def 10 ; :: thesis: verum