theorem Th11: :: MATRIX14:11

for K being Field
for x, y1, y2 being FinSequence of K
for a being Element of K st len x = len y1 & len x = len y2 holds
|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|