let L be non empty right_complementable add-associative right_zeroed right-distributive unital 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:25;
now :: thesis: for i being Element of NAT st i in dom F & i <> 1 holds
F /. i = 0. L
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:25;
then i > 0 + 1 by A6, XXREAL_0:1;
then i - 1 > 0 by XREAL_1:20;
then A7: i -' 1 > 0 by XREAL_0:def 2;
thus F /. i = F . i by A5, PARTFUN1:def 6
.= (p . (i -' 1)) * ((power L) . ((0. L),(i -' 1))) by A3, A5
.= (p . (i -' 1)) * (0. L) by A7, VECTSP_1:36
.= 0. L ; :: thesis: verum
end;
hence eval (p,(0. L)) = F /. 1 by A1, A4, POLYNOM2:3
.= F . 1 by A4, PARTFUN1:def 6
.= (p . (1 -' 1)) * ((power L) . ((0. L),(1 -' 1))) by A3, A4
.= (p . (1 -' 1)) * ((power L) . ((0. L),0)) by XREAL_1:232
.= (p . (1 -' 1)) * (1_ L) by GROUP_1:def 7
.= p . (1 -' 1) by GROUP_1:def 4
.= p . 0 by XREAL_1:232 ;
:: thesis: verum
end;
suppose len F = 0 ; :: thesis: eval (p,(0. L)) = p . 0
then A8: p = 0_. L by A2, POLYNOM4:5;
hence eval (p,(0. L)) = 0. L by POLYNOM4:17
.= p . 0 by A8, FUNCOP_1:7 ;
:: thesis: verum
end;
end;