theorem LMThGM25: :: ZMODLAT2:68

for i, j being Nat
for K being Field
for aj, bj being Element of K
for A, B being Element of (i -VectSp_over K) st j in Seg i & aj = A . j & bj = B . j holds
(A + B) . j = aj + bj