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 ;
then A6: dom ((Line (A,i)) + (Line (B,i))) = Seg () by ;
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 () by Th25;
then A9: ( [i,j] in Indices A & (Line (A,i)) . j = A * (i,j) ) by ;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
(Line (B,i)) . j = B * (i,j) by ;
then ((Line (A,i)) . j) + ((Line (B,i)) . j) = (A + B) * (i,j) by ;
hence ((Line (A,i)) + (Line (B,i))) . j = (A + B) * (i,j) by ; :: thesis: verum
end;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by ; :: thesis: verum