theorem Th3: :: BAGORDER:4

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