for K being Field
for f1, f2 being FinSequence of K holds
( dom (mlt (f1,f2)) = (dom f1) /\ (dom f2) & ( for i being Element of NAT st i in dom (mlt (f1,f2)) holds
(mlt (f1,f2)) . i = (f1 /. i) * (f2 /. i) ) )