for fs being FinSequence of NAT holds
( Sum fs = 0 iff fs = (len fs) |-> 0 )