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 <= width A holds
Col (A + B),i = (Col A,i) + (Col B,i) )
assume A1: ( len A = len B & width A = width B ) ; :: thesis: for i being Nat st 1 <= i & i <= width A holds
Col (A + B),i = (Col A,i) + (Col B,i)
let i be Nat; :: thesis: ( 1 <= i & i <= width A implies Col (A + B),i = (Col A,i) + (Col B,i) )
assume ( 1 <= i & i <= width A ) ; :: thesis: Col (A + B),i = (Col A,i) + (Col B,i)
then A2: i in Seg (width A) by FINSEQ_1:3;
A3: len (Col A,i) = len A by MATRIX_1:def 9;
A4: len (Col B,i) = len B by MATRIX_1:def 9;
A5: len (A + B) = len A by Th25;
A6: len ((Col A,i) + (Col B,i)) = len (Col A,i) by A1, A3, A4, EUCLID_2:6;
Seg (len (A + B)) = dom (A + B) by FINSEQ_1:def 3;
then A7: dom ((Col A,i) + (Col B,i)) = dom (A + B) by A3, A5, A6, FINSEQ_1:def 3;
A8: dom A = dom B by A1, FINSEQ_3:31;
for j being Nat st j in dom (A + B) holds
((Col A,i) + (Col B,i)) . j = (A + B) * j,i

proof

let j be Nat; :: thesis: ( j in dom (A + B) implies ((Col A,i) + (Col B,i)) . j = (A + B) * j,i )
assume A9: j in dom (A + B) ; :: thesis: ((Col A,i) + (Col B,i)) . j = (A + B) * j,i
then j in Seg (len (A + B)) by FINSEQ_1:def 3;
then A10: j in dom A by A5, FINSEQ_1:def 3;
then A11: [j,i] in Indices A by A2, ZFMISC_1:106;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A12: (Col A,i) . j = A * j,i by A10, MATRIX_1:def 9;
(Col B,i) . j = B * j,i by A8, A10, MATRIX_1:def 9;
then ((Col A,i) . j) + ((Col B,i) . j) = (A + B) * j,i by A11, A12, Th25;
hence ((Col A,i) + (Col B,i)) . j = (A + B) * j,i by A7, A9, VALUED_1:def 1; :: thesis: verum

end;

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