let i be Nat; :: thesis: for K being Field
for j being Element of NAT
for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds
Line (A + B),i = (Line A,i) + (Line B,i)
let K be Field; :: thesis: for j being Element of NAT
for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds
Line (A + B),i = (Line A,i) + (Line B,i)
let j be Element of NAT ; :: thesis: for A, B being Matrix of K st width A = width B & ex j being Element of NAT st [i,j] in Indices A holds
Line (A + B),i = (Line A,i) + (Line B,i)
let A, B be Matrix of K; :: thesis: ( width A = width B & ex j being Element of NAT st [i,j] in Indices A implies Line (A + B),i = (Line A,i) + (Line B,i) )
assume that
A1: width A = width B and
A2: ex j being Element of NAT st [i,j] in Indices A ; :: thesis: Line (A + B),i = (Line A,i) + (Line B,i)
reconsider a = Line A,i, b = Line B,i as Element of (width A) -tuples_on the carrier of K by A1;
A3: width (A + B) = width A by MATRIX_3:def 3;
i in dom A by A2, ZFMISC_1:106;
then A4: i in Seg (len A) by FINSEQ_1:def 3;
A5: len (A + B) = len A by MATRIX_3:def 3;
then A6: Indices (A + B) = Indices A by A3, Th55;
A7: for k being Nat st 1 <= k & k <= len (Line (A + B),i) holds
(Line (A + B),i) . k = ((Line A,i) + (Line B,i)) . k

proof

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

end;

A16: len ((Line A,i) + (Line B,i)) = len (a + b)
.= width A by FINSEQ_1:def 18 ;
len (Line (A + B),i) = width A by A3, MATRIX_1:def 8;
hence Line (A + B),i = (Line A,i) + (Line B,i) by A16, A7, FINSEQ_1:18; :: thesis: verum