let L be non empty right_complementable add-associative right_zeroed unital right-distributive doubleLoopStr ; :: thesis: for p being Polynomial of L holds eval p,(0. L) = p . 0
let p be Polynomial of L; :: thesis: eval p,(0. L) = p . 0
consider F being FinSequence of the carrier of L such that
A1: eval p,(0. L) = Sum F and
A2: len F = len p and
A3: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (0. L),(n -' 1)) by POLYNOM4:def 2;

per cases ( len F > 0 or len F = 0 ) ;

suppose len F > 0 ; :: thesis: eval p,(0. L) = p . 0

then 0 + 1 <= len F by NAT_1:13;
then A4: 1 in dom F by FINSEQ_3:27;

now

let i be Element of NAT ; :: thesis: ( i in dom F & i <> 1 implies F /. i = 0. L )
assume that
A5: i in dom F and
A6: i <> 1 ; :: thesis: F /. i = 0. L
0 + 1 <= i by A5, FINSEQ_3:27;
then i > 0 + 1 by A6, XXREAL_0:1;
then i - 1 > 0 by XREAL_1:22;
then A7: i -' 1 > 0 by XREAL_0:def 2;
thus F /. i = F . i by A5, PARTFUN1:def 8
.= (p . (i -' 1)) * ((power L) . (0. L),(i -' 1)) by A3, A5
.= (p . (i -' 1)) * (0. L) by A7, VECTSP_1:95
.= 0. L by VECTSP_1:36 ; :: thesis: verum

end;

hence eval p,(0. L) = F /. 1 by A1, A4, POLYNOM2:5
.= F . 1 by A4, PARTFUN1:def 8
.= (p . (1 -' 1)) * ((power L) . (0. L),(1 -' 1)) by A3, A4
.= (p . (1 -' 1)) * ((power L) . (0. L),0 ) by XREAL_1:234
.= (p . (1 -' 1)) * (1_ L) by GROUP_1:def 8
.= p . (1 -' 1) by GROUP_1:def 5
.= p . 0 by XREAL_1:234 ;
:: thesis: verum

end;

suppose len F = 0 ; :: thesis: eval p,(0. L) = p . 0

then A8: p = 0_. L by A2, POLYNOM4:8;
hence eval p,(0. L) = 0. L by POLYNOM4:20
.= p . 0 by A8, FUNCOP_1:13 ;
:: thesis: verum

end;

end;