theorem Th75: :: MATRIXJ1:75

for K being Field
for A being Matrix of K
for G being FinSequence_of_Matrix of K holds <*A*> (#) G = <*(A * (G . 1))*>