theorem Th68: :: MATRIXJ1:68

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