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_0:def 7;
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:25;
A4: width (A + B) = width A by Th25;
len (Line (B,i)) = width B by MATRIX_0:def 7;
then A5: len ((Line (A,i)) + (Line (B,i))) = len (Line (A,i)) by A1, A2, RVSUM_1:115;
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_0:def 7, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
(Line (B,i)) . j = B * (i,j) by A1, A8, MATRIX_0:def 7;
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_0:def 7; :: thesis: verum