for i being Nat
for K being Field
for j being Nat
for A, B being Matrix of K st width A = width B & ex j being Nat st [i,j] in Indices A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))