theorem Th14: :: MATRIX_3:14

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