let A, B be Matrix of REAL ; :: 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 ( 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:27;
A3: len (Line A,i) = width A by MATRIX_1:def 8;
A4: len (Line B,i) = width B by MATRIX_1:def 8;
A5: width (A + B) = width A by Th25;
A6: len ((Line A,i) + (Line B,i)) = len (Line A,i) by A1, A3, A4, EUCLID_2:6;
then A7: dom ((Line A,i) + (Line B,i)) = Seg (width A) by A3, 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 A8: j in Seg (width (A + B)) ; :: thesis: ((Line A,i) + (Line B,i)) . j = (A + B) * i,j
then A9: j in Seg (width A) by Th25;
then A10: [i,j] in Indices A by A2, ZFMISC_1:106;
A11: (Line A,i) . j = A * i,j by A9, MATRIX_1:def 8;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
(Line B,i) . j = B * i,j by A1, A9, MATRIX_1:def 8;
then ((Line A,i) . j) + ((Line B,i) . j) = (A + B) * i,j by A10, A11, Th25;
hence ((Line A,i) + (Line B,i)) . j = (A + B) * i,j by A5, A7, A8, VALUED_1:def 1; :: thesis: verum

end;

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