for RFin being FinSequence of REAL st len RFin = 0 holds
Sum RFin = 0