theorem Th50: :: FVSUM_1:50

for i being Nat
for K being non empty multMagma
for a, a9 being Element of K
for p being FinSequence of the carrier of K st i in dom (a * p) & a9 = p . i holds
(a * p) . i = a * a9