theorem LM03: :: LOPBAN11:2

for R1, R2 being FinSequence of REAL
for n, i being Nat
for r being Real st i in dom R1 & R1 = n |-> 1 & R2 = R1 +* (i,r) holds
Product R2 = r