theorem Th1: :: UPROOTS:1

for f being FinSequence of NAT st ( for i being Element of NAT st i in dom f holds
f . i <> 0 ) holds
( Sum f = len f iff f = (len f) |-> 1 )