theorem Th60: :: MATRIX_4:60
for K being Ring
for j being Nat
for A, B being Matrix of K st len A = len B & j in Seg (width A) holds
Col ((A + B),j) = (Col (A,j)) + (Col (B,j))