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 holds
( ( j in dom (mlt (p,q)) implies ( ( i = j implies (mlt (p,q)) . j = q . i ) & ( i <> j implies (mlt (p,q)) . j = 0. K ) ) ) & ( j in dom (mlt (q,p)) implies ( ( i = j implies (mlt (q,p)) . j = q . i ) & ( i <> j implies (mlt (q,p)) . j = 0. K ) ) ) )