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