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