theorem Th12: :: NAT_5:12

for f1, f2 being FinSequence of REAL st f2 = f1 - {0} holds
Sum f1 = Sum f2