theorem Th59: :: MATRIX_4:59

for i being Nat
for K being Ring
for j being Nat
for A, B being Matrix of K st width A = width B & i in dom A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))