theorem Th30: :: MATRLIN2:30

for j being Nat
for K being Field
for V1 being finite-dimensional VectSp of K
for b1 being OrdBasis of V1
for B1 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len p2 & len p1 = len B1 & len p1 > 0 & j in dom b1 & ( for i being Nat st i in dom p2 holds
p2 . i = ((B1 /. i) |-- b1) . j ) holds
p1 "*" p2 = ((Sum (lmlt (p1,B1))) |-- b1) . j