theorem LMXFIN1: :: ASYMPT_2:26

for x being XFinSequence of REAL
for y being Real_Sequence holds
( x (#) y is finite Sequence of REAL & dom (x (#) y) = dom x & ( for i being object st i in dom x holds
(x (#) y) . i = (x . i) * (y . i) ) )