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

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 A2: [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
A3: ( Indices (Segm (A + B),nt,mt) = Indices (Segm A,nt,mt) & Indices (Segm A,nt,mt) = Indices (Segm B,nt,mt) ) by MATRIX_1:27;
A4: [(nt . i),(mt . j)] in Indices A by A1, A2, A3, MATRIX13:17;
reconsider nti = nt . i, mtj = mt . j as Nat by VALUED_0:12;
thus (Segm (A + B),nt,mt) * i,j = (A + B) * nti,mtj by A2, MATRIX13:def 1
.= (A * nti,mtj) + (B * nti,mtj) by A4, MATRIX_3:def 3
.= ((Segm A,nt,mt) * i,j) + (B * nti,mtj) by A2, A3, MATRIX13:def 1
.= ((Segm A,nt,mt) * i,j) + ((Segm B,nt,mt) * i,j) by A2, A3, MATRIX13:def 1
.= ((Segm A,nt,mt) + (Segm B,nt,mt)) * i,j by A2, A3, 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