let R be Ring; :: thesis: for p being Polynomial of R holds (<%(0. R),(1. R)%> *' p) . 0 = 0. R
let p be Polynomial of R; :: thesis: (<%(0. R),(1. R)%> *' p) . 0 = 0. R
set q = <%(0. R),(1. R)%>;
consider r being FinSequence of the carrier of R such that
A: ( len r = 0 + 1 & (<%(0. R),(1. R)%> *' p) . 0 = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (<%(0. R),(1. R)%> . (k -' 1)) * (p . ((0 + 1) -' k)) ) ) by POLYNOM3:def 9;
dom r = {1} by FINSEQ_1:2, A, FINSEQ_1:def 3;
then 1 in dom r by TARSKI:def 1;
then C: r . 1 = (<%(0. R),(1. R)%> . (1 -' 1)) * (p . ((0 + 1) -' 1)) by A
.= (<%(0. R),(1. R)%> . 0) * (p . (1 -' 1)) by NAT_2:8
.= (<%(0. R),(1. R)%> . 0) * (p . 0) by NAT_2:8
.= (0. R) * (p . 0) by POLYNOM5:38 ;
r = <*(r . 1)*> by A, FINSEQ_1:40;
hence (<%(0. R),(1. R)%> *' p) . 0 = 0. R by A, C, RLVECT_1:44; :: thesis: verum