let A, B be Matrix of REAL ; :: 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) )
A2: len (Line A,i) = width A by MATRIX_1:def 8;
assume ( 1 <= i & i <= len A ) ; :: thesis: Line (A + B),i = (Line A,i) + (Line B,i)
then A3: i in dom A by FINSEQ_3:27;
A4: width (A + B) = width A by Th25;
len (Line B,i) = width B by MATRIX_1:def 8;
then A5: len ((Line A,i) + (Line B,i)) = len (Line A,i) by A1, A2, RVSUM_1:145;
then A6: dom ((Line A,i) + (Line B,i)) = Seg (width A) by A2, FINSEQ_1:def 3;
for j being Nat st j in Seg (width (A + B)) holds
((Line A,i) + (Line B,i)) . j = (A + B) * i,j

proof

let j be Nat; :: thesis: ( j in Seg (width (A + B)) implies ((Line A,i) + (Line B,i)) . j = (A + B) * i,j )
assume A7: j in Seg (width (A + B)) ; :: thesis: ((Line A,i) + (Line B,i)) . j = (A + B) * i,j
then A8: j in Seg (width A) by Th25;
then A9: ( [i,j] in Indices A & (Line A,i) . j = A * i,j ) by A3, MATRIX_1:def 8, ZFMISC_1:106;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
(Line B,i) . j = B * i,j by A1, A8, MATRIX_1:def 8;
then ((Line A,i) . j) + ((Line B,i) . j) = (A + B) * i,j by A9, Th25;
hence ((Line A,i) + (Line B,i)) . j = (A + B) * i,j by A4, A6, A7, VALUED_1:def 1; :: thesis: verum

end;

hence Line (A + B),i = (Line A,i) + (Line B,i) by A2, A4, A5, MATRIX_1:def 8; :: thesis: verum