theorem Th24: :: RLVECT_2:24

for i being Nat
for V being RealLinearSpace
for v being VECTOR of V
for F being FinSequence of V
for f being Function of the carrier of V,REAL st i in dom F & v = F . i holds
(f (#) F) . i = (f . v) * v