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:3;
then [i,(width A1)] in Indices A1 by A2, ZFMISC_1:87;
hence Line ((A1 + A2),i) = (Line (A1,i)) + (Line (A2,i)) by A1, MATRIX_4:59; :: thesis: verum

end;

end;