let i be Nat; :: thesis: for K being Field
for A1, A2 being Matrix of K st width A1 = width A2 & i in dom A1 holds
Line (A1 + A2),i = (Line A1,i) + (Line A2,i)
let K be Field; :: thesis: for A1, A2 being Matrix of K st width A1 = width A2 & i in dom A1 holds
Line (A1 + A2),i = (Line A1,i) + (Line A2,i)
let A1, A2 be Matrix of K; :: thesis: ( width A1 = width A2 & i in dom A1 implies Line (A1 + A2),i = (Line A1,i) + (Line A2,i) )
assume that
A1: width A1 = width A2 and
A2: i in dom A1 ; :: thesis: Line (A1 + A2),i = (Line A1,i) + (Line A2,i)
reconsider L1 = Line A1,i, L2 = Line A2,i as Element of (width A1) -tuples_on the carrier of K by A1;

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

suppose A3: width A1 = 0 ; :: thesis: Line (A1 + A2),i = (Line A1,i) + (Line A2,i)

then width (A1 + A2) = 0 by MATRIX_3:def 3;
then Line (A1 + A2),i = <*> the carrier of K
.= L1 + L2 by A3 ;
hence Line (A1 + A2),i = (Line A1,i) + (Line A2,i) ; :: thesis: verum

end;

suppose width A1 > 0 ; :: thesis: Line (A1 + A2),i = (Line A1,i) + (Line A2,i)

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

end;

end;