theorem Th1: :: VECTSP11:1

for m, n being Nat
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))