let A, B be Matrix of REAL; :: thesis: ( len A = len 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 ; :: thesis: for i being Nat st 1 <= i & i <= width A holds
Col ((A + B),i) = (Col (A,i)) + (Col (B,i))
then A2: dom A = dom B by FINSEQ_3:29;
let i be Nat; :: thesis: ( 1 <= i & i <= width A implies Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) )
A3: len (Col (A,i)) = len A by MATRIX_0:def 8;
len (Col (B,i)) = len B by MATRIX_0:def 8;
then A4: len ((Col (A,i)) + (Col (B,i))) = len (Col (A,i)) by A1, A3, RVSUM_1:115;
assume ( 1 <= i & i <= width A ) ; :: thesis: Col ((A + B),i) = (Col (A,i)) + (Col (B,i))
then A5: i in Seg (width A) by FINSEQ_1:1;
A6: len (A + B) = len A by Th25;
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, A6, A4, FINSEQ_1:def 3;
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 A8: 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 A9: j in dom A by A6, FINSEQ_1:def 3;
then A10: [j,i] in Indices A by A5, ZFMISC_1:87;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
( (Col (A,i)) . j = A * (j,i) & (Col (B,i)) . j = B * (j,i) ) by A2, A9, MATRIX_0:def 8;
then ((Col (A,i)) . j) + ((Col (B,i)) . j) = (A + B) * (j,i) by A10, Th25;
hence ((Col (A,i)) + (Col (B,i))) . j = (A + B) * (j,i) by A7, A8, VALUED_1:def 1; :: thesis: verum

end;

hence Col ((A + B),i) = (Col (A,i)) + (Col (B,i)) by A3, A6, A4, MATRIX_0:def 8; :: thesis: verum