let K be Field; :: thesis: for j being Nat
for A, B being Matrix of K st len A = len B & width A = width B & ex i being Nat st [i,j] in Indices A holds
Col (A + B),j = (Col A,j) + (Col B,j)
let j be Nat; :: thesis: for A, B being Matrix of K st len A = len B & width A = width B & ex i being Nat st [i,j] in Indices A holds
Col (A + B),j = (Col A,j) + (Col B,j)
let A, B be Matrix of K; :: thesis: ( len A = len B & width A = width B & ex i being Nat st [i,j] in Indices A implies Col (A + B),j = (Col A,j) + (Col B,j) )
assume A1: ( len A = len B & width A = width B ) ; :: thesis: ( for i being Nat holds not [i,j] in Indices A or Col (A + B),j = (Col A,j) + (Col B,j) )
given i being Nat such that A2: [i,j] in Indices A ; :: thesis: Col (A + B),j = (Col A,j) + (Col B,j)
A3: ( len (A + B) = len A & width (A + B) = width A ) by MATRIX_3:def 3;
then A4: Indices (A + B) = Indices A by Th55;
reconsider a = Col A,j, b = Col B,j as Element of (len A) -tuples_on the carrier of K by A1;
A5: len ((Col A,j) + (Col B,j)) = len (a + b)
.= len A by FINSEQ_1:def 18 ;
A6: len (Col (A + B),j) = len A by A3, MATRIX_1:def 9;
for k being Nat st 1 <= k & k <= len (Col (A + B),j) holds
(Col (A + B),j) . k = ((Col A,j) + (Col B,j)) . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len (Col (A + B),j) implies (Col (A + B),j) . k = ((Col A,j) + (Col B,j)) . k )
assume A7: ( 1 <= k & k <= len (Col (A + B),j) ) ; :: thesis: (Col (A + B),j) . k = ((Col A,j) + (Col B,j)) . k
A8: len (Col (A + B),j) = len A by A3, MATRIX_1:def 9;
A9: len (Col A,j) = len A by MATRIX_1:def 9;
A10: len (Col B,j) = len B by MATRIX_1:def 9;
k in Seg (len A) by A7, A8, FINSEQ_1:3;
then A11: ( k in dom (A + B) & j in Seg (width (A + B)) ) by A2, A3, FINSEQ_1:def 3, ZFMISC_1:106;
then A12: [k,j] in Indices (A + B) by ZFMISC_1:106;
A13: (Col (A + B),j) . k = (A + B) * k,j by A11, MATRIX_1:def 9
.= (A * k,j) + (B * k,j) by A4, A12, MATRIX_3:def 3 ;
A14: k in Seg (len (Col A,j)) by A7, A8, A9, FINSEQ_1:3;
then k in dom (Col A,j) by FINSEQ_1:def 3;
then reconsider d = (Col A,j) . k as Element of K by FINSEQ_2:13;
k in Seg (len (Col B,j)) by A1, A7, A8, A10, FINSEQ_1:3;
then k in dom (Col B,j) by FINSEQ_1:def 3;
then reconsider e = (Col B,j) . k as Element of K by FINSEQ_2:13;
len ((Col A,j) + (Col B,j)) = len (a + b)
.= len A by FINSEQ_1:def 18
.= len (Col A,j) by FINSEQ_1:def 18 ;
then k in dom ((Col A,j) + (Col B,j)) by A14, FINSEQ_1:def 3;
then A15: ((Col A,j) + (Col B,j)) . k = d + e by FVSUM_1:21;
A16: dom A = Seg (len A) by FINSEQ_1:def 3
.= dom B by A1, FINSEQ_1:def 3 ;
A17: k in dom A by A9, A14, FINSEQ_1:def 3;
then (Col A,j) . k = A * k,j by MATRIX_1:def 9;
hence (Col (A + B),j) . k = ((Col A,j) + (Col B,j)) . k by A13, A15, A16, A17, MATRIX_1:def 9; :: thesis: verum

end;

hence Col (A + B),j = (Col A,j) + (Col B,j) by A5, A6, FINSEQ_1:18; :: thesis: verum