theorem :: NUMBER17:44

for f being 1 -element natural-valued positive FinSequence ex a being positive Nat st f = <*a*>