theorem Th45: :: NUMBER17:45

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