for rF being real-valued XFinSequence st rF is nonnegative-yielding holds
( Sum rF = 0 iff ( len rF = 0 or rF = (len rF) --> 0 ) )