let m, n 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 :: thesis: for i, j being Nat st [i,j] in Indices (Segm ((A + B),nt,mt)) holds
(Segm ((A + B),nt,mt)) * (i,j) = ((Segm (A,nt,mt)) + (Segm (B,nt,mt))) * (i,j)

A2: Indices (Segm (A,nt,mt)) = Indices (Segm (B,nt,mt)) by MATRIX_0:26;
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_0:26;
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_0:27; :: thesis: verum