theorem :: FVSUM_1:60

for i being Nat
for K being non empty multMagma
for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (mlt (p1,p2)) & a1 = p1 . i & a2 = p2 . i holds
(mlt (p1,p2)) . i = a1 * a2 by FUNCOP_1:22;