theorem Th17: :: MATRIX_3:17

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 & Sum (mlt (q,p)) = q . i )