theorem Th9: :: MATRLIN2:9

for K being Field
for V1 being finite-dimensional VectSp of K
for R1, R2 being FinSequence of V1
for p1, p2 being FinSequence of K st len p1 = len R1 & len p2 = len R2 holds
lmlt ((p1 ^ p2),(R1 ^ R2)) = (lmlt (p1,R1)) ^ (lmlt (p2,R2))