let K be Field; :: thesis: for A, B being Matrix of K st width A = width B holds
for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let A, B be Matrix of K; :: thesis: ( width A = width B implies for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume A1: width A = width B ; :: thesis: for i being Nat st 1 <= i & i <= len A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume ( 1 <= i & i <= len A ) ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
then A2: i in dom A by FINSEQ_3:25;
reconsider LB = Line (B,i) as Element of (width A) -tuples_on the carrier of K by A1;

per cases ( width A > 0 or width A = 0 ) ;

suppose width A > 0 ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

then width A in Seg (width A) by FINSEQ_1:3;
then [i,(width A)] in Indices A by A2, ZFMISC_1:87;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A1, MATRIX_4:59; :: thesis: verum

end;

suppose A3: width A = 0 ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))

then len ((Line (A,i)) + LB) = 0 ;
then A4: (Line (A,i)) + (Line (B,i)) = {} ;
width (A + B) = 0 by A3, MATRIX_3:def 3;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A4; :: thesis: verum

end;

end;