theorem LMThGM24: :: ZMODLAT2:67

for i, j being Nat
for K being Field
for a, aj being Element of K
for R being Element of (i -VectSp_over K) st j in Seg i & aj = R . j holds
(a * R) . j = a * aj