theorem Th18: :: MFOLD_2:18

for n being Nat
for F being FinSequence of (TOP-REAL n)
for fr being Function of (TOP-REAL n),REAL
for Fv being FinSequence of (RealVectSpace (Seg n))
for fv being Function of (RealVectSpace (Seg n)),REAL st fr = fv & F = Fv holds
fr (#) F = fv (#) Fv