let i be Nat; :: thesis: for K being Ring
for j being Nat
for A, B being Matrix of K st width A = width B & i in dom A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let K be Ring; :: thesis: for j being Nat
for A, B being Matrix of K st width A = width B & i in dom A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let j be Nat; :: thesis: for A, B being Matrix of K st width A = width B & i in dom A holds
Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
let A, B be Matrix of K; :: thesis: ( width A = width B & i in dom A implies Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) )
assume that
A1: width A = width B and
A2: i in dom A ; :: thesis: Line ((A + B),i) = (Line (A,i)) + (Line (B,i))
reconsider wA = width A as Element of NAT by ORDINAL1:def 12;
reconsider a = Line (A,i), b = Line (B,i) as Element of wA -tuples_on the carrier of K by A1;
A3: width (A + B) = width A by MATRIX_3:def 3;
A4: i in Seg (len A) by A2, 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_0:def 7;
then A10: k in Seg (width (A + B)) by A3, A8, FINSEQ_1:1;
len (Line (B,i)) = width B by MATRIX_0:def 7;
then k in Seg (len (Line (B,i))) by A1, A8, A9, FINSEQ_1:1;
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:11;
i in dom (A + B) by A5, A4, FINSEQ_1:def 3;
then A11: [i,k] in Indices (A + B) by A10, ZFMISC_1:87;
A12: (Line ((A + B),i)) . k = (A + B) * (i,k) by A10, MATRIX_0:def 7
.= (A * (i,k)) + (B * (i,k)) by A6, A11, MATRIX_3:def 3 ;
A13: len (Line (A,i)) = width A by MATRIX_0:def 7;
then A14: k in Seg (len (Line (A,i))) by A8, A9, FINSEQ_1:1;
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:11;
len ((Line (A,i)) + (Line (B,i))) = len (a + b)
.= width A by CARD_1:def 7
.= len (Line (A,i)) by CARD_1:def 7 ;
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:17;
(Line (A,i)) . k = A * (i,k) by A13, A14, MATRIX_0:def 7;
hence (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k by A1, A13, A12, A14, A15, MATRIX_0:def 7; :: thesis: verum

end;

A16: len ((Line (A,i)) + (Line (B,i))) = len (a + b)
.= width A by CARD_1:def 7 ;
len (Line ((A + B),i)) = width A by A3, MATRIX_0:def 7;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by A16, A7, FINSEQ_1:14; :: thesis: verum