theorem Th4: :: MATRTOP2:4

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