let n, m be Nat; :: thesis: for K being Field
for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt)
let K be Field; :: thesis: for A, B being Matrix of K
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt)
let A, B be Matrix of K; :: thesis: for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt)
let nt be Element of n -tuples_on NAT ; :: thesis: for mt being Element of m -tuples_on NAT st [:(rng nt),(rng mt):] c= Indices A holds
Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt)
let mt be Element of m -tuples_on NAT ; :: thesis: ( [:(rng nt),(rng mt):] c= Indices A implies Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt) )
assume A1: [:(rng nt),(rng mt):] c= Indices A ; :: thesis: Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt)

now

A2: Indices (Segm A,nt,mt) = Indices (Segm B,nt,mt) by MATRIX_1:27;
let i, j be Nat; :: thesis: ( [i,j] in Indices (Segm (A + B),nt,mt) implies (Segm (A + B),nt,mt) * i,j = ((Segm A,nt,mt) + (Segm B,nt,mt)) * i,j )
assume A3: [i,j] in Indices (Segm (A + B),nt,mt) ; :: thesis: (Segm (A + B),nt,mt) * i,j = ((Segm A,nt,mt) + (Segm B,nt,mt)) * i,j
reconsider nti = nt . i, mtj = mt . j as Nat by VALUED_0:12;
A4: Indices (Segm (A + B),nt,mt) = Indices (Segm A,nt,mt) by MATRIX_1:27;
then A5: [(nt . i),(mt . j)] in Indices A by A1, A3, MATRIX13:17;
thus (Segm (A + B),nt,mt) * i,j = (A + B) * nti,mtj by A3, MATRIX13:def 1
.= (A * nti,mtj) + (B * nti,mtj) by A5, MATRIX_3:def 3
.= ((Segm A,nt,mt) * i,j) + (B * nti,mtj) by A3, A4, MATRIX13:def 1
.= ((Segm A,nt,mt) * i,j) + ((Segm B,nt,mt) * i,j) by A3, A4, A2, MATRIX13:def 1
.= ((Segm A,nt,mt) + (Segm B,nt,mt)) * i,j by A3, A4, MATRIX_3:def 3 ; :: thesis: verum

end;

hence Segm (A + B),nt,mt = (Segm A,nt,mt) + (Segm B,nt,mt) by MATRIX_1:28; :: thesis: verum