let i be Nat; :: thesis: for K being Field
for j being Nat
for A, B being Matrix of K st width A = width B & ex j being 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 Nat
for A, B being Matrix of K st width A = width B & ex j being Nat st [i,j] in Indices 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 & ex j being 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 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 Nat st [i,j] in Indices 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;
i in dom A by ;
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 ;
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 ;
then A10: k in Seg (width (A + B)) by ;
len (Line (B,i)) = width B by MATRIX_0:def 7;
then k in Seg (len (Line (B,i))) by ;
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 ;
then A11: [i,k] in Indices (A + B) by ;
A12: (Line ((A + B),i)) . k = (A + B) * (i,k) by
.= (A * (i,k)) + (B * (i,k)) by ;
A13: len (Line (A,i)) = width A by MATRIX_0:def 7;
then A14: k in Seg (len (Line (A,i))) by ;
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 ;
then A15: ((Line (A,i)) + (Line (B,i))) . k = d + e by FVSUM_1:17;
(Line (A,i)) . k = A * (i,k) by ;
hence (Line ((A + B),i)) . k = ((Line (A,i)) + (Line (B,i))) . k by ; :: 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 ;
hence Line ((A + B),i) = (Line (A,i)) + (Line (B,i)) by ; :: thesis: verum