let R be Ring; :: thesis: for p being Polynomial of R
for i being Nat holds (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i
let p be Polynomial of R; :: thesis: for i being Nat holds (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i
let i be Nat; :: thesis: (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i
set q = <%(0. R),(1. R)%>;
consider r being FinSequence of the carrier of R such that
A: ( len r = (i + 1) + 1 & (<%(0. R),(1. R)%> *' p) . (i + 1) = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (<%(0. R),(1. R)%> . (k -' 1)) * (p . (((i + 1) + 1) -' k)) ) ) by POLYNOM3:def 9;
B: dom r = Seg (i + 2) by A, FINSEQ_1:def 3;
C: Seg 2 c= dom r by B, FINSEQ_1:5, NAT_1:11;
D: 2 in dom r by C, FINSEQ_1:3;
H2: 2 - 2 <= (i + 2) - 2 by NAT_1:11, XREAL_1:9;
H3: 0 <= 2 - 1 ;
E: r /. 2 = r . 2 by D, PARTFUN1:def 6
.= (<%(0. R),(1. R)%> . (2 -' 1)) * (p . (((i + 1) + 1) -' 2)) by D, A
.= (<%(0. R),(1. R)%> . 1) * (p . (((i + 1) + 1) -' 2)) by H3, XREAL_0:def 2
.= (<%(0. R),(1. R)%> . 1) * (p . i) by H2, XREAL_0:def 2
.= (1. R) * (p . i) by POLYNOM5:38 ;
F: now :: thesis: for k being Element of NAT st k in dom r & k <> 2 holds
r /. k = 0. R
let k be Element of NAT ; :: thesis: ( k in dom r & k <> 2 implies r /. b1 = 0. R )
assume F: ( k in dom r & k <> 2 ) ; :: thesis: r /. b1 = 0. R
per cases then ( k < 2 or k > 2 ) by XXREAL_0:1;
suppose k < 2 ; :: thesis: r /. b1 = 0. R
then k + 1 <= 2 by INT_1:7;
then F4: (k + 1) - 1 <= 2 - 1 by XREAL_1:9;
F5: 1 <= k by F, B, FINSEQ_1:1;
then F3: k = 1 by F4, XXREAL_0:1;
F2: k -' 1 = k - 1 by F5, XREAL_0:def 2;
thus r /. k = r . k by F, PARTFUN1:def 6
.= (<%(0. R),(1. R)%> . (k -' 1)) * (p . (((i + 1) + 1) -' k)) by A, F
.= (0. R) * (p . (((i + 1) + 1) -' k)) by F3, F2, POLYNOM5:38
.= 0. R ; :: thesis: verum
end;
suppose F4: k > 2 ; :: thesis: r /. b1 = 0. R
then 2 + 1 <= k by INT_1:7;
then F3: (2 + 1) - 1 <= k - 1 by XREAL_1:9;
F2: k - 1 = k -' 1 by F4, XREAL_0:def 2;
thus r /. k = r . k by F, PARTFUN1:def 6
.= (<%(0. R),(1. R)%> . (k -' 1)) * (p . (((i + 1) + 1) -' k)) by A, F
.= (0. R) * (p . (((i + 1) + 1) -' k)) by F2, F3, POLYNOM5:38
.= 0. R ; :: thesis: verum
end;
end;
end;
thus (<%(0. R),(1. R)%> *' p) . (i + 1) = p . i by E, A, D, F, POLYNOM2:3; :: thesis: verum