theorem Th19: :: MFOLD_2:19

for n being Nat
for F being FinSequence of (TOP-REAL n)
for Fv being FinSequence of (RealVectSpace (Seg n)) st Fv = F holds
Sum F = Sum Fv