for K being Ring
for p, q being FinSequence of K
for i being Nat st i in dom p & i in dom q & p . i = 1. K & ( for k being Nat st k in dom p & k <> i holds
p . k = 0. K ) holds
Sum (mlt (p,q)) = q . i