:: deftheorem Def9 defines *' POLYNOM3:def 9 :
for L being non empty doubleLoopStr
for p, q, b₄ being sequence of L holds
( b₄ = p *' q iff for i being Element of NAT ex r being FinSequence of the carrier of L st
( len r = i + 1 & b₄ . i = Sum r & ( for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) );