theorem Th64: :: MATRIXJ1:64

for K being Field
for G, G1 being FinSequence_of_Matrix of K
for p, p1 being FinSequence of K st len G = len p & len G1 <= len p1 holds
mlt ((p ^ p1),(G ^ G1)) = (mlt (p,G)) ^ (mlt (p1,G1))