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)

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

hence
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
by A2, A4, A5, MATRIX_0:def 7; :: thesis: verum
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;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