let p1, q1 be sequence of INT.Ring; :: thesis: (p1 *' q1) . 0 = (p1 . 0) * (q1 . 0)
consider r being FinSequence of the carrier of INT.Ring such that
A1: ( len r = 0 + 1 & (p1 *' q1) . 0 = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p1 . (k -' 1)) * (q1 . ((0 + 1) -' k)) ) ) by POLYNOM3:def 9;
A2: r = <*(r . 1)*> by A1, FINSEQ_1:40;
dom r = Seg 1 by A1, FINSEQ_1:def 3;
then 1 in dom r ;
then r . 1 = (p1 . (1 -' 1)) * (q1 . ((0 + 1) -' 1)) by A1
.= (p1 . 0) * (q1 . (0 + 0)) ;
hence (p1 *' q1) . 0 = (p1 . 0) * (q1 . 0) by A1, A2, RLVECT_1:44; :: thesis: verum