let K be Field; :: thesis: for A, B being Matrix of K st len A = len B & 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: ( len A = len B & 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: ( len A = len B & 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 A2: ( 1 <= i & i <= len A ) ; :: thesis: Line (A + B),i = (Line A,i) + (Line B,i)
A3: i in dom A by A2, FINSEQ_3:27;
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:5;
then [i,(width A)] in Indices A by A3, ZFMISC_1:106;
hence Line (A + B),i = (Line A,i) + (Line B,i) by A1, MATRIX_4:59; :: thesis: verum

end;

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

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

end;

end;