theorem Th21: :: REAL_NS2:21

for n being Nat
for Ft being FinSequence of (TOP-REAL n)
for Fr being FinSequence of (REAL-NS n) st Ft = Fr holds
Sum Ft = Sum Fr